N (lemma)
NAddOrderPropFunct.add_le_cases [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_lt_mono [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_cases [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_le_mono [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_repl_pair [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_cases [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_pos [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_add_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_le_add_le [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_lt_add_lt [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_add_pos_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_add_pos_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_le_add_lt [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_lt_add_l [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_lt_add_r [in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddPropFunct.add_assoc [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_cancel_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_cancel_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_comm [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_dichotomy [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_pred_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_pred_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_shuffle1 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_shuffle2 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_succ_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_succ_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_wd [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_0_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_0_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_1_l [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_1_r [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_succ [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_0 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_1 [in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.succ_add_discr [in Coq.Numbers.Natural.Abstract.NAdd]
natlike_ind [in Coq.ZArith.Wf_Z]
natlike_rec [in Coq.ZArith.Wf_Z]
natlike_rec2 [in Coq.ZArith.Wf_Z]
natlike_rec3 [in Coq.ZArith.Wf_Z]
Nat_as_OT.lt_not_eq [in Coq.FSets.OrderedTypeEx]
Nat_as_OT.lt_trans [in Coq.FSets.OrderedTypeEx]
nat_case [in Coq.Init.Peano]
nat_compare_eq [in Coq.Arith.Compare_dec]
nat_compare_ge [in Coq.Arith.Compare_dec]
nat_compare_gt [in Coq.Arith.Compare_dec]
nat_compare_le [in Coq.Arith.Compare_dec]
nat_compare_lt [in Coq.Arith.Compare_dec]
nat_compare_S [in Coq.Arith.Compare_dec]
nat_double_ind [in Coq.Init.Peano]
nat_of_Ncompare [in Coq.NArith.Nnat]
nat_of_Ndiv2 [in Coq.NArith.Nnat]
nat_of_Ndouble [in Coq.NArith.Nnat]
nat_of_Ndouble_plus_one [in Coq.NArith.Nnat]
nat_of_Nmax [in Coq.NArith.Nnat]
nat_of_Nmin [in Coq.NArith.Nnat]
nat_of_Nminus [in Coq.NArith.Nnat]
nat_of_Nmult [in Coq.NArith.Nnat]
nat_of_Nplus [in Coq.NArith.Nnat]
nat_of_Nsucc [in Coq.NArith.Nnat]
nat_of_N_of_nat [in Coq.NArith.Nnat]
nat_of_P_gt_Gt_compare_complement_morphism [in Coq.NArith.Pnat]
nat_of_P_gt_Gt_compare_morphism [in Coq.NArith.Pnat]
nat_of_P_inj [in Coq.NArith.Pnat]
nat_of_P_lt_Lt_compare_complement_morphism [in Coq.NArith.Pnat]
nat_of_P_lt_Lt_compare_morphism [in Coq.NArith.Pnat]
nat_of_P_minus_morphism [in Coq.NArith.Pnat]
nat_of_P_mult_morphism [in Coq.NArith.Pnat]
nat_of_P_o_P_of_succ_nat_eq_succ [in Coq.NArith.Pnat]
nat_of_P_plus_carry_morphism [in Coq.NArith.Pnat]
nat_of_P_plus_morphism [in Coq.NArith.Pnat]
nat_of_P_succ_morphism [in Coq.NArith.Pnat]
nat_of_P_xH [in Coq.NArith.Pnat]
nat_of_P_xI [in Coq.NArith.Pnat]
nat_of_P_xO [in Coq.NArith.Pnat]
nat_total_order [in Coq.Arith.Lt]
NBasePropFunct.case_analysis [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.double_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_dec [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_dne [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_pred_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.if_zero_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.if_zero_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.induction [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.le_0_l [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_refl [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_succ_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_sym [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_sym [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_trans [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0_r [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pair_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_inj [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_wd [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_0 [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj_wd [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj_wd_neg [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_pred [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_wd [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.two_dim_induction [in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.zero_or_succ [in Coq.Numbers.Natural.Abstract.NBase]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_eq_cases [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_irrefl [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_succ_r [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmax_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmax_r [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmin_l [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmin_r [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.pred_0 [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_succ [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_wd [in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_0 [in Coq.Numbers.Natural.Binary.NBinDefs]
Nbit0_Blow [in Coq.NArith.Ndigits]
Nbit0_correct [in Coq.NArith.Ndigits]
Nbit0_gt [in Coq.NArith.Ndigits]
Nbit0_less [in Coq.NArith.Ndigits]
Nbit0_neq [in Coq.NArith.Ndec]
Nbit_Bth [in Coq.NArith.Ndigits]
Nbit_faithful [in Coq.NArith.Ndigits]
Nbit_faithful_1 [in Coq.NArith.Ndigits]
Nbit_faithful_2 [in Coq.NArith.Ndigits]
Nbit_faithful_3 [in Coq.NArith.Ndigits]
Nbit_faithful_4 [in Coq.NArith.Ndigits]
Nbit_Nsize [in Coq.NArith.Ndigits]
Ncompare_antisym [in Coq.NArith.BinNat]
Ncompare_eq_correct [in Coq.NArith.BinNat]
Ncompare_Eq_eq [in Coq.NArith.BinNat]
Ncompare_Neqb [in Coq.NArith.Ndec]
Ncompare_n_Sm [in Coq.NArith.BinNat]
Ncompare_refl [in Coq.NArith.BinNat]
Ncompare_0 [in Coq.NArith.BinNat]
Ndiv2_bit_eq [in Coq.NArith.Ndec]
Ndiv2_bit_neq [in Coq.NArith.Ndec]
Ndiv2_correct [in Coq.NArith.Ndigits]
Ndiv2_double [in Coq.NArith.Ndigits]
Ndiv2_double_plus_one [in Coq.NArith.Ndigits]
Ndiv2_eq [in Coq.NArith.Ndec]
Ndiv2_neq [in Coq.NArith.Ndec]
Ndiv_eucl_correct [in Coq.ZArith.ZOdiv_def]
Ndiv_Z0div [in Coq.ZArith.ZOdiv]
Ndouble_bit0 [in Coq.NArith.Ndigits]
Ndouble_div2 [in Coq.NArith.BinNat]
Ndouble_inj [in Coq.NArith.BinNat]
Ndouble_or_double_plus_un [in Coq.NArith.Ndec]
Ndouble_plus_one_bit0 [in Coq.NArith.Ndigits]
Ndouble_plus_one_div2 [in Coq.NArith.BinNat]
Ndouble_plus_one_inj [in Coq.NArith.BinNat]
negative_derivative [in Coq.Reals.MVT]
negb_andb [in Coq.Bool.Bool]
negb_if [in Coq.Bool.Bool]
negb_involutive [in Coq.Bool.Bool]
negb_involutive_reverse [in Coq.Bool.Bool]
negb_orb [in Coq.Bool.Bool]
negb_prop_classical [in Coq.Bool.Bool]
negb_prop_elim [in Coq.Bool.Bool]
negb_prop_intro [in Coq.Bool.Bool]
negb_prop_involutive [in Coq.Bool.Bool]
negb_sym [in Coq.Bool.Bool]
neg_cos [in Coq.Reals.Rtrigo]
neg_false [in Coq.Init.Logic]
neg_pos_Rsqr_le [in Coq.Reals.R_sqr]
neg_sin [in Coq.Reals.Rtrigo]
neighbourhood_P1 [in Coq.Reals.Rtopology]
Neqb_comm [in Coq.NArith.Ndec]
Neqb_complete [in Coq.NArith.Ndec]
Neqb_correct [in Coq.NArith.Ndec]
Neqb_Ncompare [in Coq.NArith.Ndec]
nequiv_equiv_trans [in Coq.Classes.SetoidClass]
neq_O_lt [in Coq.Arith.Lt]
Neven_not_double_plus_one [in Coq.NArith.Ndec]
Newman [in Coq.Sets.Relations_3_facts]
NewtonInt_P1 [in Coq.Reals.NewtonInt]
NewtonInt_P2 [in Coq.Reals.NewtonInt]
NewtonInt_P3 [in Coq.Reals.NewtonInt]
NewtonInt_P4 [in Coq.Reals.NewtonInt]
NewtonInt_P5 [in Coq.Reals.NewtonInt]
NewtonInt_P6 [in Coq.Reals.NewtonInt]
NewtonInt_P7 [in Coq.Reals.NewtonInt]
NewtonInt_P8 [in Coq.Reals.NewtonInt]
NewtonInt_P9 [in Coq.Reals.NewtonInt]
nil_cons [in Coq.Lists.List]
nil_cons [in Coq.Lists.MonoList]
ni_le_antisym [in Coq.NArith.Ndist]
ni_le_le [in Coq.NArith.Ndist]
ni_le_min_induc [in Coq.NArith.Ndist]
ni_le_min_1 [in Coq.NArith.Ndist]
ni_le_min_2 [in Coq.NArith.Ndist]
ni_le_refl [in Coq.NArith.Ndist]
ni_le_total [in Coq.NArith.Ndist]
ni_le_trans [in Coq.NArith.Ndist]
ni_min_assoc [in Coq.NArith.Ndist]
ni_min_case [in Coq.NArith.Ndist]
ni_min_comm [in Coq.NArith.Ndist]
ni_min_idemp [in Coq.NArith.Ndist]
ni_min_inf_l [in Coq.NArith.Ndist]
ni_min_inf_r [in Coq.NArith.Ndist]
ni_min_O_l [in Coq.NArith.Ndist]
ni_min_O_r [in Coq.NArith.Ndist]
Nleb_antisym [in Coq.NArith.Ndec]
Nleb_double_mono [in Coq.NArith.Ndec]
Nleb_double_mono_conv [in Coq.NArith.Ndec]
Nleb_double_plus_one_mono [in Coq.NArith.Ndec]
Nleb_double_plus_one_mono_conv [in Coq.NArith.Ndec]
Nleb_ltb_trans [in Coq.NArith.Ndec]
Nleb_Nle [in Coq.NArith.Ndec]
Nleb_refl [in Coq.NArith.Ndec]
Nleb_trans [in Coq.NArith.Ndec]
Nless_def_1 [in Coq.NArith.Ndigits]
Nless_def_2 [in Coq.NArith.Ndigits]
Nless_def_3 [in Coq.NArith.Ndigits]
Nless_def_4 [in Coq.NArith.Ndigits]
Nless_not_refl [in Coq.NArith.Ndigits]
Nless_total [in Coq.NArith.Ndigits]
Nless_trans [in Coq.NArith.Ndigits]
Nless_z [in Coq.NArith.Ndigits]
Nltb_double_mono [in Coq.NArith.Ndec]
Nltb_double_mono_conv [in Coq.NArith.Ndec]
Nltb_double_plus_one_mono [in Coq.NArith.Ndec]
Nltb_double_plus_one_mono_conv [in Coq.NArith.Ndec]
Nltb_leb_trans [in Coq.NArith.Ndec]
Nltb_leb_weak [in Coq.NArith.Ndec]
Nltb_trans [in Coq.NArith.Ndec]
Nlt_irrefl [in Coq.NArith.BinNat]
Nminus_N0_Nle [in Coq.NArith.BinNat]
Nminus_succ_r [in Coq.NArith.BinNat]
Nminus_0_r [in Coq.NArith.BinNat]
Nmin_choice [in Coq.NArith.Ndec]
Nmin_le_1 [in Coq.NArith.Ndec]
Nmin_le_2 [in Coq.NArith.Ndec]
Nmin_le_3 [in Coq.NArith.Ndec]
Nmin_le_4 [in Coq.NArith.Ndec]
Nmin_le_5 [in Coq.NArith.Ndec]
Nmin_lt_3 [in Coq.NArith.Ndec]
Nmin_lt_4 [in Coq.NArith.Ndec]
Nmin_Nmin' [in Coq.NArith.Ndec]
Nmod_lt [in Coq.ZArith.ZOdiv]
Nmod_Z0mod [in Coq.ZArith.ZOdiv]
NMulOrderPropFunct.eq_mul_0 [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_0_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_0_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_1 [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_square_0 [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.lt_0_mul [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.lt_1_mul_pos [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_cancel_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_cancel_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_id_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_id_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_pos_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_pos_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono_pos_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono_pos_r [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_pred [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_pos_pos [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_2_mono_l [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.neq_mul_0 [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.square_le_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.square_lt_mono [in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulPropFunct.add_mul_repl_pair [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_add_distr_l [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_add_distr_r [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_assoc [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_comm [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_succ_l [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_succ_r [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_wd [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_0_l [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_0_r [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_1_l [in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_1_r [in Coq.Numbers.Natural.Abstract.NMul]
Nmult_assoc [in Coq.NArith.BinNat]
Nmult_comm [in Coq.NArith.BinNat]
Nmult_plus_distr_r [in Coq.NArith.BinNat]
Nmult_reg_r [in Coq.NArith.BinNat]
Nmult_Sn_m [in Coq.NArith.BinNat]
Nmult_0_l [in Coq.NArith.BinNat]
Nmult_1_l [in Coq.NArith.BinNat]
Nmult_1_r [in Coq.NArith.BinNat]
Nneg_bit0 [in Coq.NArith.Ndigits]
Nneg_bit0_1 [in Coq.NArith.Ndigits]
Nneg_bit0_2 [in Coq.NArith.Ndigits]
Nneq_elim [in Coq.NArith.Ndec]
Nnot_div2_not_double [in Coq.NArith.Ndec]
Nnot_div2_not_double_plus_one [in Coq.NArith.Ndec]
NNPP [in Coq.Logic.Classical_Prop]
Nodd_not_double [in Coq.NArith.Ndec]
NodepOfDep.add_1 [in Coq.FSets.FSetBridge]
NodepOfDep.add_2 [in Coq.FSets.FSetBridge]
NodepOfDep.add_3 [in Coq.FSets.FSetBridge]
NodepOfDep.cardinal_1 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_1 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_2 [in Coq.FSets.FSetBridge]
NodepOfDep.choose_3 [in Coq.FSets.FSetBridge]
NodepOfDep.compat_P_aux [in Coq.FSets.FSetBridge]
NodepOfDep.diff_1 [in Coq.FSets.FSetBridge]
NodepOfDep.diff_2 [in Coq.FSets.FSetBridge]
NodepOfDep.diff_3 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_1 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_2 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_3 [in Coq.FSets.FSetBridge]
NodepOfDep.elements_3w [in Coq.FSets.FSetBridge]
NodepOfDep.empty_1 [in Coq.FSets.FSetBridge]
NodepOfDep.equal_1 [in Coq.FSets.FSetBridge]
NodepOfDep.equal_2 [in Coq.FSets.FSetBridge]
NodepOfDep.exists_1 [in Coq.FSets.FSetBridge]
NodepOfDep.exists_2 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_1 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_2 [in Coq.FSets.FSetBridge]
NodepOfDep.filter_3 [in Coq.FSets.FSetBridge]
NodepOfDep.fold_1 [in Coq.FSets.FSetBridge]
NodepOfDep.for_all_1 [in Coq.FSets.FSetBridge]
NodepOfDep.for_all_2 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_1 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_2 [in Coq.FSets.FSetBridge]
NodepOfDep.inter_3 [in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_1 [in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_2 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_1 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_2 [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_3 [in Coq.FSets.FSetBridge]
NodepOfDep.mem_1 [in Coq.FSets.FSetBridge]
NodepOfDep.mem_2 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_1 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_2 [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_3 [in Coq.FSets.FSetBridge]
NodepOfDep.partition_1 [in Coq.FSets.FSetBridge]
NodepOfDep.partition_2 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_1 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_2 [in Coq.FSets.FSetBridge]
NodepOfDep.remove_3 [in Coq.FSets.FSetBridge]
NodepOfDep.singleton_1 [in Coq.FSets.FSetBridge]
NodepOfDep.singleton_2 [in Coq.FSets.FSetBridge]
NodepOfDep.subset_1 [in Coq.FSets.FSetBridge]
NodepOfDep.subset_2 [in Coq.FSets.FSetBridge]
NodepOfDep.union_1 [in Coq.FSets.FSetBridge]
NodepOfDep.union_2 [in Coq.FSets.FSetBridge]
NodepOfDep.union_3 [in Coq.FSets.FSetBridge]
NoDupA_app [in Coq.Lists.SetoidList]
NoDupA_equivlistA_permut [in Coq.Sorting.PermutSetoid]
NoDupA_rev [in Coq.Lists.SetoidList]
NoDupA_split [in Coq.Lists.SetoidList]
NoDupA_swap [in Coq.Lists.SetoidList]
NoDup_permut [in Coq.Sorting.PermutEq]
NoDup_Permutation [in Coq.Lists.List]
NoDup_remove_1 [in Coq.Lists.List]
NoDup_remove_2 [in Coq.Lists.List]
Noetherian_contains_Noetherian [in Coq.Sets.Relations_3_facts]
nonneg_derivative_0 [in Coq.Reals.Ranalysis1]
nonneg_derivative_1 [in Coq.Reals.MVT]
nonpos_derivative_0 [in Coq.Reals.MVT]
nonpos_derivative_1 [in Coq.Reals.MVT]
non_dep_dep_functional_choice [in Coq.Logic.ChoiceFacts]
non_dep_dep_functional_rel_reification [in Coq.Logic.ChoiceFacts]
Non_disjoint_union [in Coq.Sets.Powerset_facts]
Non_disjoint_union' [in Coq.Sets.Powerset_facts]
Noone_in_empty [in Coq.Sets.Constructive_sets]
NOrderPropFunct.eq_le_incl [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.eq_0_gt_0_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.gt_wf [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.left_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.left_induction' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_antisymm [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_dec [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_dne [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ge_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_gt_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ind [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ind_rel [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_le_succ_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_lt_trans [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_neq [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ngt [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_le [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_le_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_refl [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_diag_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_trans [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_wd [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_0_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_0_1 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_1_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_asymm [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_dec [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_dne [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_eq_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_exists_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ge_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_gt_cases [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ind [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ind_rel [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_irrefl [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_incl [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_trans [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_succ_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_neq [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_nge [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_le [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_lt [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_lt_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_diag_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_iter_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_lt_pred [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_trans [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_trichotomy [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wd [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wf [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wf_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_0_succ [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_0_1 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_1_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_1_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_wd [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_wd [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_diag_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_diag_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_iter_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_0_lt_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_gt [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_succ_diag_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_succ_0 [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_ge [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_succ_diag_l [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_succ_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_0_r [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.order_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.order_induction' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.pred_le_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.pred_lt_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.right_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.right_induction' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_left_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_left_induction' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_right_induction [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_right_induction' [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_le_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_lt_mono [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_pred_pos [in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.zero_one [in Coq.Numbers.Natural.Abstract.NOrder]
not_all_ex_not [in Coq.Logic.Classical_Pred_Set]
not_all_ex_not [in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [in Coq.Logic.Classical_Pred_Set]
not_and [in Coq.Logic.Decidable]
not_and_iff [in Coq.Logic.Decidable]
not_and_or [in Coq.Logic.Classical_Prop]
not_Empty_Add [in Coq.Sets.Constructive_sets]
not_empty_Inhabited [in Coq.Sets.Classical_sets]
not_eq [in Coq.Arith.Compare_dec]
not_eq_S [in Coq.Init.Peano]
not_even_and_odd [in Coq.Arith.Even]
not_ex_all_not [in Coq.Logic.Classical_Pred_Set]
not_ex_all_not [in Coq.Logic.Classical_Pred_Type]
not_ex_not_all [in Coq.Logic.Classical_Pred_Set]
not_ex_not_all [in Coq.Logic.Classical_Pred_Type]
not_false_iff [in Coq.Logic.Decidable]
not_false_is_true [in Coq.Bool.Bool]
not_ge [in Coq.Arith.Compare_dec]
not_gt [in Coq.Arith.Compare_dec]
not_has_fixpoint [in Coq.Logic.Berardi]
not_iff [in Coq.Logic.Decidable]
not_imp [in Coq.Logic.Decidable]
not_imply_elim [in Coq.Logic.Classical_Prop]
not_imply_elim2 [in Coq.Logic.Classical_Prop]
not_imp_iff [in Coq.Logic.Decidable]
not_imp_rev_iff [in Coq.Logic.Decidable]
not_included_empty_Inhabited [in Coq.Sets.Classical_sets]
not_injective_elim [in Coq.Sets.Image]
not_INR [in Coq.Reals.RIneq]
not_Isnil_cons [in Coq.Lists.TheoryList]
not_le [in Coq.Arith.Compare_dec]
not_le_minus_0 [in Coq.Arith.Minus]
not_lt [in Coq.Arith.Compare_dec]
not_not [in Coq.Logic.Decidable]
not_not_archimedean [in Coq.Reals.Rlogic]
not_not_iff [in Coq.Logic.Decidable]
not_or [in Coq.Logic.Decidable]
not_or_and [in Coq.Logic.Classical_Prop]
not_or_iff [in Coq.Logic.Decidable]
not_prime_divide [in Coq.ZArith.Znumtheory]
not_prime_0 [in Coq.ZArith.Znumtheory]
not_prime_1 [in Coq.ZArith.Znumtheory]
not_rel_prime_0 [in Coq.ZArith.Znumtheory]
not_Rlt [in Coq.Reals.SeqProp]
not_SIncl_empty [in Coq.Sets.Classical_sets]
not_true_iff [in Coq.Logic.Decidable]
not_true_is_false [in Coq.Bool.Bool]
not_Zeq [in Coq.ZArith.Zorder]
not_Zeq_inf [in Coq.ZArith.ZArith_dec]
not_0_INR [in Coq.Reals.RIneq]
not_0_IZR [in Coq.Reals.RIneq]
not_1_INR [in Coq.Reals.RIneq]
no_fixpoint_negb [in Coq.Bool.Bool]
Npdist_comm [in Coq.NArith.Ndist]
Npdist_eq_1 [in Coq.NArith.Ndist]
Npdist_eq_2 [in Coq.NArith.Ndist]
Npdist_ultra [in Coq.NArith.Ndist]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_eq_cases [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_irrefl [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_succ_r [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmax_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmax_r [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmin_l [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmin_r [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.pred_0 [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_succ [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_wd [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_0 [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.succ_neq_0 [in Coq.Numbers.Natural.Peano.NPeano]
NPgeb_correct [in Coq.ZArith.ZOdiv_def]
NPgeb_Zge [in Coq.ZArith.ZOdiv]
NPgeb_Zlt [in Coq.ZArith.ZOdiv]
Nplength_first_one [in Coq.NArith.Ndist]
Nplength_infty [in Coq.NArith.Ndist]
Nplength_lb [in Coq.NArith.Ndist]
Nplength_one [in Coq.NArith.Ndist]
Nplength_ub [in Coq.NArith.Ndist]
Nplength_ultra [in Coq.NArith.Ndist]
Nplength_ultra_1 [in Coq.NArith.Ndist]
Nplength_zeros [in Coq.NArith.Ndist]
Nplus_assoc [in Coq.NArith.BinNat]
Nplus_comm [in Coq.NArith.BinNat]
Nplus_reg_l [in Coq.NArith.BinNat]
Nplus_succ [in Coq.NArith.BinNat]
Nplus_0_l [in Coq.NArith.BinNat]
Nplus_0_r [in Coq.NArith.BinNat]
Npred_succ [in Coq.NArith.BinNat]
Nrect_base [in Coq.NArith.BinNat]
Nrect_step [in Coq.NArith.BinNat]
Nrec_base [in Coq.NArith.BinNat]
Nrec_step [in Coq.NArith.BinNat]
Nsame_bit0 [in Coq.NArith.Ndigits]
nshiftl_above_size [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_n_0 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_size [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S_tail [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_above_size [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_n_0 [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_predsize_0_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_size [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S_tail [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_firstl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_propagates [in Coq.Numbers.Cyclic.Int31.Cyclic31]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.BS [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.B0 [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.B_holds [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_eq_cases [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_irrefl [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_succ_r [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmax_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmax_r [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmin_l [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmin_r [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_compare_alt [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_le [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_lt [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_max [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_min [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.pred_0 [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_succ [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_wd [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_0 [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSubPropFunct.add_sub [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_assoc [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_nz [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_swap [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.le_sub_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_pred_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_sub_distr_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_sub_distr_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_add [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_add_distr [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_diag [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_gt [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_wd [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_l [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_le [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_r [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_1_r [in Coq.Numbers.Natural.Abstract.NSub]
Nsucc_inj [in Coq.NArith.BinNat]
Nsucc_0 [in Coq.NArith.BinNat]
Nth [in Coq.Lists.TheoryList]
ntheq_eqst [in Coq.Lists.Streams]
nth_In [in Coq.Lists.List]
nth_indep [in Coq.Lists.List]
nth_in_or_default [in Coq.Lists.List]
nth_le [in Coq.Arith.Between]
nth_le_length [in Coq.Lists.TheoryList]
nth_lt_O [in Coq.Lists.TheoryList]
nth_overflow [in Coq.Lists.List]
nth_S_cons [in Coq.Lists.List]
null_derivative_loc [in Coq.Reals.MVT]
null_derivative_0 [in Coq.Reals.MVT]
null_derivative_1 [in Coq.Reals.MVT]
nu_left_inv [in Coq.Logic.Eqdep_dec]
Nxor_assoc [in Coq.NArith.Ndigits]
Nxor_bit0 [in Coq.NArith.Ndigits]
Nxor_BVxor [in Coq.NArith.Ndigits]
Nxor_comm [in Coq.NArith.Ndigits]
Nxor_div2 [in Coq.NArith.Ndigits]
Nxor_eq [in Coq.NArith.Ndigits]
Nxor_eq_false [in Coq.NArith.Ndec]
Nxor_eq_true [in Coq.NArith.Ndec]
Nxor_neutral_left [in Coq.NArith.Ndigits]
Nxor_neutral_right [in Coq.NArith.Ndigits]
Nxor_nilpotent [in Coq.NArith.Ndigits]
Nxor_semantics [in Coq.NArith.Ndigits]
Nxor_sem_1 [in Coq.NArith.Ndigits]
Nxor_sem_2 [in Coq.NArith.Ndigits]
Nxor_sem_3 [in Coq.NArith.Ndigits]
Nxor_sem_4 [in Coq.NArith.Ndigits]
Nxor_sem_5 [in Coq.NArith.Ndigits]
Nxor_sem_6 [in Coq.NArith.Ndigits]
NZAddOrderPropFunct.NZadd_le_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_lt_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_le_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_neg_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_nonneg [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_pos [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonpos_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_cases [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_nonneg [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_pos [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZle_le_add_le [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZle_lt_add_lt [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_add_pos_l [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_add_pos_r [in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_le_add_lt [in Coq.Numbers.NatInt.NZAddOrder]
NZAddPropFunct.NZadd_assoc [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_cancel_l [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_cancel_r [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_comm [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_shuffle1 [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_shuffle2 [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_succ_r [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_0_r [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_1_l [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_1_r [in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZsub_1_r [in Coq.Numbers.NatInt.NZAdd]
NZBasePropFunct.NZcentral_induction [in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZE_stepl [in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZneq_sym [in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj [in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj_wd [in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj_wd_neg [in Coq.Numbers.NatInt.NZBase]
NZCyclicAxiomsMod.BS [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B0 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B_holds [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_0 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_1 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZadd_succ_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZadd_0_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZeq_equiv [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZinduction [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZmul_succ_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZmul_0_l [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZpred_mod_wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZpred_succ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsub_succ_r [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsub_0_r [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsucc_mod_wB [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z_mod [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Z_to_NZ_0 [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZMulOrderPropFunct.NZeq_mul_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_mul_0_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_mul_0_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_square_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZlt_0_mul [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZlt_1_mul_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_cancel_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_cancel_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_id_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_id_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_neg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_neg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonpos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonpos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_pos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_pos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_neg_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_neg_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_pos_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_pos_r [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_pred [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_neg_neg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_neg_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_pos_neg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_pos_pos [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_2_mono_l [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZneq_mul_0 [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_le_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_le_simpl_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_lt_mono_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_lt_simpl_nonneg [in Coq.Numbers.NatInt.NZMulOrder]
NZMulPropFunct.NZmul_add_distr_l [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_add_distr_r [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_assoc [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_comm [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_succ_r [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_0_r [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_1_l [in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_1_r [in Coq.Numbers.NatInt.NZMul]
NZOrderPropFunct.NZAcc_gt_wd [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZAcc_lt_wd [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZA'A_left [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZA'A_right [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_dec [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_le_incl [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZgt_wf [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlbase [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZleft_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZleft_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_antisymm [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_dec [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ge_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_gt_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ind [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_le_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_lt_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_neq [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ngt [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_refl [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_stepl [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_stepr [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_0_1 [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZls'_ls'' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZls_ls' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_asymm [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_dec [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_dne [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_exists_pred [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_exists_pred_strong [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_ge_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_gt_cases [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_ind [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_le_incl [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_le_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_lt_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_neq [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_nge [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_stepl [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_stepr [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_iter_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_trans [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_trichotomy [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_wf [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_0_1 [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_1_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_diag_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_iter_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnle_gt [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnle_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_ge [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_succ_diag_l [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_succ_r [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction'_0 [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction_0 [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrbase [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZright_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZright_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrs'_rs'' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrs_rs' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_left_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_left_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_right_induction [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_right_induction' [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZsucc_le_mono [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZsucc_lt_mono [in Coq.Numbers.NatInt.NZOrder]
Nzorn [in Coq.Reals.RiemannInt_SF]
N0_less_1 [in Coq.NArith.Ndigits]
N0_less_2 [in Coq.NArith.Ndigits]
N2Bv_Bv2N [in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen [in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen_above [in Coq.NArith.Ndigits]
N_as_OT.lt_not_eq [in Coq.FSets.OrderedTypeEx]
N_div_mod_eq [in Coq.ZArith.ZOdiv]
N_ind_double [in Coq.NArith.BinNat]
N_of_div2 [in Coq.NArith.Nnat]
N_of_double [in Coq.NArith.Nnat]
N_of_double_plus_one [in Coq.NArith.Nnat]
N_of_max [in Coq.NArith.Nnat]
N_of_min [in Coq.NArith.Nnat]
N_of_minus [in Coq.NArith.Nnat]
N_of_mult [in Coq.NArith.Nnat]
N_of_nat_compare [in Coq.NArith.Nnat]
N_of_nat_of_N [in Coq.NArith.Nnat]
N_of_plus [in Coq.NArith.Nnat]
N_of_S [in Coq.NArith.Nnat]
N_rec_double [in Coq.NArith.BinNat]
n_Sn [in Coq.Init.Peano]
n_SSn [in Coq.Arith.Plus]
n_SSSn [in Coq.Arith.Plus]
n_SSSSn [in Coq.Arith.Plus]