Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13562 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (96 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (210 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (71 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6947 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (306 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (351 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (182 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (295 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2870 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (286 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (433 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1189 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (326 entries)

N

N [inductive, in Coq.NArith.BinNat]
N [module, in Coq.Logic.Eqdep_dec]
NAdd [library]
NAddOrder [library]
NAddOrderPropFunct [module, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_cases [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_le_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_cases [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_lt_repl_pair [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_cases [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_pos [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.add_pos_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_add_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_le_add_le [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.le_lt_add_lt [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_add_pos_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_add_pos_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_le_add_lt [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_lt_add_l [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropFunct.lt_lt_add_r [lemma, in Coq.Numbers.Natural.Abstract.NAddOrder]
NAddOrderPropMod [module, in Coq.Numbers.Natural.Abstract.NMulOrder]
NAddPropFunct [module, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_assoc [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_cancel_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_cancel_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_comm [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_dichotomy [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_pred_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_shuffle1 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_shuffle2 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_wd [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_0_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_0_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_1_l [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.add_1_r [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_succ [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_0 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.eq_add_1 [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropFunct.succ_add_discr [lemma, in Coq.Numbers.Natural.Abstract.NAdd]
NAddPropMod [module, in Coq.Numbers.Natural.Abstract.NMul]
napply_cst [definition, in Coq.Numbers.NaryFunctions]
napply_discard [definition, in Coq.Numbers.NaryFunctions]
napply_except_last [definition, in Coq.Numbers.NaryFunctions]
napply_then_last [definition, in Coq.Numbers.NaryFunctions]
NArith [library]
NaryFunctions [library]
nat [inductive, in Coq.Init.Datatypes]
natinf [inductive, in Coq.NArith.Ndist]
natlike_ind [lemma, in Coq.ZArith.Wf_Z]
natlike_rec [lemma, in Coq.ZArith.Wf_Z]
natlike_rec2 [lemma, in Coq.ZArith.Wf_Z]
natlike_rec3 [lemma, in Coq.ZArith.Wf_Z]
NatSeq [section, in Coq.Lists.List]
Nat_as_DT [module, in Coq.Logic.DecidableTypeEx]
Nat_as_OT [module, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.compare [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.eq [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.eq_dec [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.eq_refl [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.eq_sym [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.eq_trans [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.lt [definition, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.lt_not_eq [lemma, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.lt_trans [lemma, in Coq.FSets.OrderedTypeEx]
Nat_as_OT.t [definition, in Coq.FSets.OrderedTypeEx]
nat_case [lemma, in Coq.Init.Peano]
nat_compare [definition, in Coq.Arith.Compare_dec]
nat_compare_eq [lemma, in Coq.Arith.Compare_dec]
nat_compare_ge [lemma, in Coq.Arith.Compare_dec]
nat_compare_gt [lemma, in Coq.Arith.Compare_dec]
nat_compare_le [lemma, in Coq.Arith.Compare_dec]
nat_compare_lt [lemma, in Coq.Arith.Compare_dec]
nat_compare_S [lemma, in Coq.Arith.Compare_dec]
nat_double_ind [lemma, in Coq.Init.Peano]
nat_eq_bool [definition, in Coq.Arith.Bool_nat]
nat_eq_eqdec [instance, in Coq.Classes.EquivDec]
nat_eq_eqdec [instance, in Coq.Classes.SetoidDec]
nat_ge_lt_bool [definition, in Coq.Arith.Bool_nat]
nat_gt_le_bool [definition, in Coq.Arith.Bool_nat]
nat_le_gt_bool [definition, in Coq.Arith.Bool_nat]
nat_lt_ge_bool [definition, in Coq.Arith.Bool_nat]
nat_noteq_bool [definition, in Coq.Arith.Bool_nat]
nat_of_ascii [definition, in Coq.Strings.Ascii]
nat_of_N [definition, in Coq.NArith.Nnat]
nat_of_Ncompare [lemma, in Coq.NArith.Nnat]
nat_of_Ndiv2 [lemma, in Coq.NArith.Nnat]
nat_of_Ndouble [lemma, in Coq.NArith.Nnat]
nat_of_Ndouble_plus_one [lemma, in Coq.NArith.Nnat]
nat_of_Nmax [lemma, in Coq.NArith.Nnat]
nat_of_Nmin [lemma, in Coq.NArith.Nnat]
nat_of_Nminus [lemma, in Coq.NArith.Nnat]
nat_of_Nmult [lemma, in Coq.NArith.Nnat]
nat_of_Nplus [lemma, in Coq.NArith.Nnat]
nat_of_Nsucc [lemma, in Coq.NArith.Nnat]
nat_of_N_of_nat [lemma, in Coq.NArith.Nnat]
nat_of_P [definition, in Coq.NArith.BinPos]
nat_of_P_gt_Gt_compare_complement_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_gt_Gt_compare_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_inj [lemma, in Coq.NArith.Pnat]
nat_of_P_lt_Lt_compare_complement_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_lt_Lt_compare_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_minus_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_mult_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_o_P_of_succ_nat_eq_succ [lemma, in Coq.NArith.Pnat]
nat_of_P_plus_carry_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_plus_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_succ_morphism [lemma, in Coq.NArith.Pnat]
nat_of_P_xH [lemma, in Coq.NArith.Pnat]
nat_of_P_xI [lemma, in Coq.NArith.Pnat]
nat_of_P_xO [lemma, in Coq.NArith.Pnat]
nat_po [definition, in Coq.Sets.Integers]
nat_total_order [lemma, in Coq.Arith.Lt]
NAxioms [library]
NAxiomsSig [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.add [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.le [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.lt [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.max [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.min [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.mul [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.N [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.Neq [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.N0 [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.N1 [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.P [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.pred_0 [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_succ [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_wd [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.recursion_0 [axiom, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.S [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NAxiomsSig.sub [abbreviation, in Coq.Numbers.Natural.Abstract.NAxioms]
NBase [library]
NBasePropFunct [module, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.case_analysis [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.DoubleInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.DoubleInduction.R [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.DoubleInduction.R_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.double_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_dec [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_dne [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.eq_pred_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.if_zero [definition, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.if_zero_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.if_zero_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.le_0_l [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_refl [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_succ_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_sym [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_sym [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.Neq_trans [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0_r [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.neq_0_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.PairInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.PairInduction.A [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.PairInduction.A_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pair_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_inj [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_wd [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.pred_0 [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj_wd [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_inj_wd_neg [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_pred [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.succ_wd [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.TwoDimensionalInduction [section, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.TwoDimensionalInduction.R [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.TwoDimensionalInduction.R_wd [variable, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.two_dim_induction [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropFunct.zero_or_succ [lemma, in Coq.Numbers.Natural.Abstract.NBase]
NBasePropMod [module, in Coq.Numbers.Natural.Abstract.NAdd]
NBasePropMod1 [module, in Coq.Numbers.Natural.Abstract.NIso]
NBasePropMod2 [module, in Coq.Numbers.Natural.Abstract.NIso]
Nbasic [library]
NBinary [library]
NBinaryAxiomsMod [module, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZ [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsucc [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZ0 [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZle [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_eq_cases [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_irrefl [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZlt_succ_r [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmax [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmax_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmax_r [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmin [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmin_l [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.NZOrdAxiomsMod.NZmin_r [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.pred_0 [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion [definition, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_succ [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_wd [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinaryAxiomsMod.recursion_0 [lemma, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinarySubPropMod [module, in Coq.Numbers.Natural.Binary.NBinDefs]
NBinDefs [library]
Nbit [definition, in Coq.NArith.Ndigits]
Nbit0 [definition, in Coq.NArith.Ndigits]
Nbit0_Blow [lemma, in Coq.NArith.Ndigits]
Nbit0_correct [lemma, in Coq.NArith.Ndigits]
Nbit0_gt [lemma, in Coq.NArith.Ndigits]
Nbit0_less [lemma, in Coq.NArith.Ndigits]
Nbit0_neq [lemma, in Coq.NArith.Ndec]
Nbit_Bth [lemma, in Coq.NArith.Ndigits]
Nbit_faithful [lemma, in Coq.NArith.Ndigits]
Nbit_faithful_1 [lemma, in Coq.NArith.Ndigits]
Nbit_faithful_2 [lemma, in Coq.NArith.Ndigits]
Nbit_faithful_3 [lemma, in Coq.NArith.Ndigits]
Nbit_faithful_4 [lemma, in Coq.NArith.Ndigits]
Nbit_Nsize [lemma, in Coq.NArith.Ndigits]
Nbound [definition, in Coq.Reals.RiemannInt_SF]
Ncompare [definition, in Coq.NArith.BinNat]
Ncompare_antisym [lemma, in Coq.NArith.BinNat]
Ncompare_eq_correct [lemma, in Coq.NArith.BinNat]
Ncompare_Eq_eq [lemma, in Coq.NArith.BinNat]
Ncompare_Neqb [lemma, in Coq.NArith.Ndec]
Ncompare_n_Sm [lemma, in Coq.NArith.BinNat]
Ncompare_refl [lemma, in Coq.NArith.BinNat]
Ncompare_0 [lemma, in Coq.NArith.BinNat]
ncurry [definition, in Coq.Numbers.NaryFunctions]
Ndec [library]
Ndigits [library]
Ndiscr [definition, in Coq.NArith.BinNat]
Ndist [library]
Ndiv [definition, in Coq.ZArith.ZOdiv_def]
Ndiv2 [definition, in Coq.NArith.BinNat]
Ndiv2_bit_eq [lemma, in Coq.NArith.Ndec]
Ndiv2_bit_neq [lemma, in Coq.NArith.Ndec]
Ndiv2_correct [lemma, in Coq.NArith.Ndigits]
Ndiv2_double [lemma, in Coq.NArith.Ndigits]
Ndiv2_double_plus_one [lemma, in Coq.NArith.Ndigits]
Ndiv2_eq [lemma, in Coq.NArith.Ndec]
Ndiv2_neq [lemma, in Coq.NArith.Ndec]
Ndiv_eucl [definition, in Coq.ZArith.ZOdiv_def]
Ndiv_eucl_correct [lemma, in Coq.ZArith.ZOdiv_def]
Ndiv_Z0div [lemma, in Coq.ZArith.ZOdiv]
Ndouble [definition, in Coq.NArith.BinNat]
Ndouble_bit0 [lemma, in Coq.NArith.Ndigits]
Ndouble_div2 [lemma, in Coq.NArith.BinNat]
Ndouble_inj [lemma, in Coq.NArith.BinNat]
Ndouble_or_double_plus_un [lemma, in Coq.NArith.Ndec]
Ndouble_plus_one [definition, in Coq.NArith.BinNat]
Ndouble_plus_one_bit0 [lemma, in Coq.NArith.Ndigits]
Ndouble_plus_one_div2 [lemma, in Coq.NArith.BinNat]
Ndouble_plus_one_inj [lemma, in Coq.NArith.BinNat]
neg [projection, in Coq.Reals.RIneq]
negative_derivative [lemma, in Coq.Reals.MVT]
negb [definition, in Coq.Init.Datatypes]
negb_andb [lemma, in Coq.Bool.Bool]
negb_elim [abbreviation, in Coq.Bool.Bool]
negb_if [lemma, in Coq.Bool.Bool]
negb_intro [abbreviation, in Coq.Bool.Bool]
negb_involutive [lemma, in Coq.Bool.Bool]
negb_involutive_reverse [lemma, in Coq.Bool.Bool]
negb_orb [lemma, in Coq.Bool.Bool]
negb_prop_classical [lemma, in Coq.Bool.Bool]
negb_prop_elim [lemma, in Coq.Bool.Bool]
negb_prop_intro [lemma, in Coq.Bool.Bool]
negb_prop_involutive [lemma, in Coq.Bool.Bool]
negb_sym [lemma, in Coq.Bool.Bool]
negreal [record, in Coq.Reals.RIneq]
neg_cos [lemma, in Coq.Reals.Rtrigo]
neg_false [lemma, in Coq.Init.Logic]
neg_pos_Rsqr_le [lemma, in Coq.Reals.R_sqr]
neg_sin [lemma, in Coq.Reals.Rtrigo]
neighbourhood [definition, in Coq.Reals.Rtopology]
neighbourhood_P1 [lemma, in Coq.Reals.Rtopology]
neq [definition, in Coq.ZArith.Znat]
Neqb [definition, in Coq.NArith.Ndec]
Neqb_comm [lemma, in Coq.NArith.Ndec]
Neqb_complete [lemma, in Coq.NArith.Ndec]
Neqb_correct [lemma, in Coq.NArith.Ndec]
Neqb_Ncompare [lemma, in Coq.NArith.Ndec]
nequiv_dec [definition, in Coq.Classes.EquivDec]
nequiv_dec [definition, in Coq.Classes.SetoidDec]
nequiv_decb [definition, in Coq.Classes.EquivDec]
nequiv_decb [definition, in Coq.Classes.SetoidDec]
nequiv_equiv_trans [lemma, in Coq.Classes.SetoidClass]
neq_O_lt [lemma, in Coq.Arith.Lt]
Neven [definition, in Coq.NArith.Ndigits]
Neven_not_double_plus_one [lemma, in Coq.NArith.Ndec]
Newman [lemma, in Coq.Sets.Relations_3_facts]
NewtonInt [definition, in Coq.Reals.NewtonInt]
NewtonInt [library]
NewtonInt_P1 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P2 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P3 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P4 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P5 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P6 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P7 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P8 [lemma, in Coq.Reals.NewtonInt]
NewtonInt_P9 [lemma, in Coq.Reals.NewtonInt]
Newton_integrable [definition, in Coq.Reals.NewtonInt]
nfold [definition, in Coq.Numbers.NaryFunctions]
nfold_bis [definition, in Coq.Numbers.NaryFunctions]
nfold_list [definition, in Coq.Numbers.NaryFunctions]
nfun [definition, in Coq.Numbers.NaryFunctions]
nfun_to_nfun [definition, in Coq.Numbers.NaryFunctions]
nfun_to_nfun_bis [definition, in Coq.Numbers.NaryFunctions]
Nge [definition, in Coq.NArith.BinNat]
Ngt [definition, in Coq.NArith.BinNat]
ni [constructor, in Coq.NArith.Ndist]
Nil [definition, in Coq.Relations.Relation_Operators]
Nil [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]
nil [constructor, in Coq.Lists.MonoList]
nil [constructor, in Coq.Lists.List]
nil [constructor, in Coq.Reals.RList]
nil_cons [lemma, in Coq.Lists.List]
nil_cons [lemma, in Coq.Lists.MonoList]
nil_is_heap [constructor, in Coq.Sorting.Heap]
nil_leA [constructor, in Coq.Sorting.Sorting]
nil_sort [constructor, in Coq.Sorting.Sorting]
Nind [definition, in Coq.NArith.BinNat]
NIso [library]
ni_le [definition, in Coq.NArith.Ndist]
ni_le_antisym [lemma, in Coq.NArith.Ndist]
ni_le_le [lemma, in Coq.NArith.Ndist]
ni_le_min_induc [lemma, in Coq.NArith.Ndist]
ni_le_min_1 [lemma, in Coq.NArith.Ndist]
ni_le_min_2 [lemma, in Coq.NArith.Ndist]
ni_le_refl [lemma, in Coq.NArith.Ndist]
ni_le_total [lemma, in Coq.NArith.Ndist]
ni_le_trans [lemma, in Coq.NArith.Ndist]
ni_min [definition, in Coq.NArith.Ndist]
ni_min_assoc [lemma, in Coq.NArith.Ndist]
ni_min_case [lemma, in Coq.NArith.Ndist]
ni_min_comm [lemma, in Coq.NArith.Ndist]
ni_min_idemp [lemma, in Coq.NArith.Ndist]
ni_min_inf_l [lemma, in Coq.NArith.Ndist]
ni_min_inf_r [lemma, in Coq.NArith.Ndist]
ni_min_O_l [lemma, in Coq.NArith.Ndist]
ni_min_O_r [lemma, in Coq.NArith.Ndist]
Nle [definition, in Coq.NArith.BinNat]
Nleb [definition, in Coq.NArith.Ndec]
Nleb_antisym [lemma, in Coq.NArith.Ndec]
Nleb_double_mono [lemma, in Coq.NArith.Ndec]
Nleb_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nleb_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nleb_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nleb_ltb_trans [lemma, in Coq.NArith.Ndec]
Nleb_Nle [lemma, in Coq.NArith.Ndec]
Nleb_refl [lemma, in Coq.NArith.Ndec]
Nleb_trans [lemma, in Coq.NArith.Ndec]
Nless [definition, in Coq.NArith.Ndigits]
Nless_aux [definition, in Coq.NArith.Ndigits]
Nless_def_1 [lemma, in Coq.NArith.Ndigits]
Nless_def_2 [lemma, in Coq.NArith.Ndigits]
Nless_def_3 [lemma, in Coq.NArith.Ndigits]
Nless_def_4 [lemma, in Coq.NArith.Ndigits]
Nless_not_refl [lemma, in Coq.NArith.Ndigits]
Nless_total [lemma, in Coq.NArith.Ndigits]
Nless_trans [lemma, in Coq.NArith.Ndigits]
Nless_z [lemma, in Coq.NArith.Ndigits]
Nlt [definition, in Coq.NArith.BinNat]
Nltb_double_mono [lemma, in Coq.NArith.Ndec]
Nltb_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nltb_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nltb_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nltb_leb_trans [lemma, in Coq.NArith.Ndec]
Nltb_leb_weak [lemma, in Coq.NArith.Ndec]
Nltb_trans [lemma, in Coq.NArith.Ndec]
Nlt_irrefl [lemma, in Coq.NArith.BinNat]
NMake [library]
Nmax [definition, in Coq.NArith.BinNat]
Nmin [definition, in Coq.NArith.BinNat]
Nminus [definition, in Coq.NArith.BinNat]
Nminus_N0_Nle [lemma, in Coq.NArith.BinNat]
Nminus_succ_r [lemma, in Coq.NArith.BinNat]
Nminus_0_r [lemma, in Coq.NArith.BinNat]
Nmin' [definition, in Coq.NArith.Ndec]
Nmin_choice [lemma, in Coq.NArith.Ndec]
Nmin_le_1 [lemma, in Coq.NArith.Ndec]
Nmin_le_2 [lemma, in Coq.NArith.Ndec]
Nmin_le_3 [lemma, in Coq.NArith.Ndec]
Nmin_le_4 [lemma, in Coq.NArith.Ndec]
Nmin_le_5 [lemma, in Coq.NArith.Ndec]
Nmin_lt_3 [lemma, in Coq.NArith.Ndec]
Nmin_lt_4 [lemma, in Coq.NArith.Ndec]
Nmin_Nmin' [lemma, in Coq.NArith.Ndec]
Nmod [definition, in Coq.ZArith.ZOdiv_def]
Nmod_lt [lemma, in Coq.ZArith.ZOdiv]
Nmod_Z0mod [lemma, in Coq.ZArith.ZOdiv]
NMul [library]
NMulOrder [library]
NMulOrderPropFunct [module, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_0 [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_0_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_0_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_mul_1 [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.eq_square_0 [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.lt_0_mul [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.lt_1_mul_pos [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_cancel_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_cancel_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_id_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_id_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_pos_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_pos_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_le_mono_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono_pos_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_mono_pos_r [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_lt_pred [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_pos [abbreviation, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_pos_pos [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.mul_2_mono_l [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.neq_mul_0 [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.square_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropFunct.square_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NMulOrder]
NMulOrderPropMod [module, in Coq.Numbers.Natural.Abstract.NSub]
NMulPropFunct [module, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.add_mul_repl_pair [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_add_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_add_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_assoc [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_comm [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_wd [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_0_l [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_0_r [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_1_l [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropFunct.mul_1_r [lemma, in Coq.Numbers.Natural.Abstract.NMul]
NMulPropMod [module, in Coq.Numbers.Natural.Abstract.NOrder]
Nmult [definition, in Coq.NArith.BinNat]
Nmult_assoc [lemma, in Coq.NArith.BinNat]
Nmult_comm [lemma, in Coq.NArith.BinNat]
Nmult_plus_distr_r [lemma, in Coq.NArith.BinNat]
Nmult_reg_r [lemma, in Coq.NArith.BinNat]
Nmult_Sn_m [lemma, in Coq.NArith.BinNat]
Nmult_0_l [lemma, in Coq.NArith.BinNat]
Nmult_1_l [lemma, in Coq.NArith.BinNat]
Nmult_1_r [lemma, in Coq.NArith.BinNat]
Nnat [library]
Nneg_bit0 [lemma, in Coq.NArith.Ndigits]
Nneg_bit0_1 [lemma, in Coq.NArith.Ndigits]
Nneg_bit0_2 [lemma, in Coq.NArith.Ndigits]
Nneq_elim [lemma, in Coq.NArith.Ndec]
Nnot_div2_not_double [lemma, in Coq.NArith.Ndec]
Nnot_div2_not_double_plus_one [lemma, in Coq.NArith.Ndec]
NNPP [lemma, in Coq.Logic.Classical_Prop]
NoConfusion [projection, in Coq.Program.Equality]
noConfusion [projection, in Coq.Program.Equality]
NoConfusionPackage [record, in Coq.Program.Equality]
Nodd [definition, in Coq.NArith.Ndigits]
Nodd_not_double [lemma, in Coq.NArith.Ndec]
NodepOfDep [module, in Coq.FSets.FSetBridge]
NodepOfDep.add [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Add [definition, in Coq.FSets.FSetBridge]
NodepOfDep.add_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.add_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.add_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.cardinal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.cardinal_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose [definition, in Coq.FSets.FSetBridge]
NodepOfDep.choose_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.choose_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.compare [definition, in Coq.FSets.FSetBridge]
NodepOfDep.compat_P_aux [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff [definition, in Coq.FSets.FSetBridge]
NodepOfDep.diff_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.diff_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements [definition, in Coq.FSets.FSetBridge]
NodepOfDep.elements_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elements_3w [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.empty_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.eq [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Equal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.equal [definition, in Coq.FSets.FSetBridge]
NodepOfDep.equal_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.equal_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.eq_dec [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_refl [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_sym [definition, in Coq.FSets.FSetBridge]
NodepOfDep.eq_trans [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Exists [definition, in Coq.FSets.FSetBridge]
NodepOfDep.exists_ [definition, in Coq.FSets.FSetBridge]
NodepOfDep.exists_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.exists_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.filter [definition, in Coq.FSets.FSetBridge]
NodepOfDep.filter_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.filter_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.filter_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.fold [definition, in Coq.FSets.FSetBridge]
NodepOfDep.fold_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.For_all [definition, in Coq.FSets.FSetBridge]
NodepOfDep.for_all [definition, in Coq.FSets.FSetBridge]
NodepOfDep.for_all_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.for_all_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.f_dec [definition, in Coq.FSets.FSetBridge]
NodepOfDep.In [definition, in Coq.FSets.FSetBridge]
NodepOfDep.inter [definition, in Coq.FSets.FSetBridge]
NodepOfDep.inter_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.inter_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.inter_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.In_1 [definition, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty [definition, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.is_empty_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.lt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.lt_not_eq [definition, in Coq.FSets.FSetBridge]
NodepOfDep.lt_trans [definition, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.max_elt_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.mem [definition, in Coq.FSets.FSetBridge]
NodepOfDep.mem_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.mem_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt [definition, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.min_elt_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.partition [definition, in Coq.FSets.FSetBridge]
NodepOfDep.partition_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.partition_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove [definition, in Coq.FSets.FSetBridge]
NodepOfDep.remove_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.remove_3 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.singleton [definition, in Coq.FSets.FSetBridge]
NodepOfDep.singleton_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.singleton_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.subset [definition, in Coq.FSets.FSetBridge]
NodepOfDep.Subset [definition, in Coq.FSets.FSetBridge]
NodepOfDep.subset_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.subset_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.t [definition, in Coq.FSets.FSetBridge]
NodepOfDep.union [definition, in Coq.FSets.FSetBridge]
NodepOfDep.union_1 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.union_2 [lemma, in Coq.FSets.FSetBridge]
NodepOfDep.union_3 [lemma, in Coq.FSets.FSetBridge]
node_is_heap [constructor, in Coq.Sorting.Heap]
NoDup [inductive, in Coq.Lists.List]
NoDupA [inductive, in Coq.Lists.SetoidList]
NoDupA_app [lemma, in Coq.Lists.SetoidList]
NoDupA_cons [constructor, in Coq.Lists.SetoidList]
NoDupA_equivlistA_permut [lemma, in Coq.Sorting.PermutSetoid]
NoDupA_nil [constructor, in Coq.Lists.SetoidList]
NoDupA_rev [lemma, in Coq.Lists.SetoidList]
NoDupA_split [lemma, in Coq.Lists.SetoidList]
NoDupA_swap [lemma, in Coq.Lists.SetoidList]
NoDup_cons [constructor, in Coq.Lists.List]
NoDup_nil [constructor, in Coq.Lists.List]
NoDup_permut [lemma, in Coq.Sorting.PermutEq]
NoDup_Permutation [lemma, in Coq.Lists.List]
NoDup_remove_1 [lemma, in Coq.Lists.List]
NoDup_remove_2 [lemma, in Coq.Lists.List]
Noetherian [definition, in Coq.Sets.Relations_3]
noetherian [inductive, in Coq.Sets.Relations_3]
Noetherian_contains_Noetherian [lemma, in Coq.Sets.Relations_3_facts]
None [constructor, in Coq.Init.Datatypes]
nonneg [projection, in Coq.Reals.RIneq]
nonnegreal [record, in Coq.Reals.RIneq]
nonneg_derivative_0 [lemma, in Coq.Reals.Ranalysis1]
nonneg_derivative_1 [lemma, in Coq.Reals.MVT]
nonpos [projection, in Coq.Reals.RIneq]
nonposreal [record, in Coq.Reals.RIneq]
nonpos_derivative_0 [lemma, in Coq.Reals.MVT]
nonpos_derivative_1 [lemma, in Coq.Reals.MVT]
nonzero [projection, in Coq.Reals.RIneq]
nonzeroreal [record, in Coq.Reals.RIneq]
non_dep_dep_functional_choice [lemma, in Coq.Logic.ChoiceFacts]
non_dep_dep_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
Non_disjoint_union [lemma, in Coq.Sets.Powerset_facts]
Non_disjoint_union' [lemma, in Coq.Sets.Powerset_facts]
Noone_in_empty [lemma, in Coq.Sets.Constructive_sets]
NOrder [library]
NOrderPropFunct [module, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.eq_le_incl [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.eq_0_gt_0_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.gt_wf [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.left_induction [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.left_induction' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_antisymm [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_dec [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_dne [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ge_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_gt_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ind [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ind_rel [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_le_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_lt_trans [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_neq [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_ngt [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_le [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_pred_le_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_refl [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_trans [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_wd [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_0_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_0_1 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.le_1_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_asymm [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_dec [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_dne [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_eq_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_eq_gt_cases [abbreviation, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_exists_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ge_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_gt_cases [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ind [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ind_rel [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_irrefl [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_incl [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_le_trans [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_lt_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_neq [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_nge [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_ngt [abbreviation, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_le [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_lt [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_pred_lt_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_iter_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_lt_pred [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_trans [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_trichotomy [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wd [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wf [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_wf_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_0_succ [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_0_1 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_1_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.lt_1_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.max_wd [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.min_wd [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_diag_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_diag_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_succ_iter_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.neq_0_lt_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_gt [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_succ_diag_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nle_succ_0 [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_ge [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_succ_diag_l [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.nlt_0_r [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.order_induction [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.order_induction' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.pred_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.pred_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.RelElim [section, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.RelElim.R [variable, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.RelElim.R_wd [variable, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.right_induction [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.right_induction' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_left_induction [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_left_induction' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_right_induction [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.strong_right_induction' [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_le_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_lt_mono [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.succ_pred_pos [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropFunct.zero_one [lemma, in Coq.Numbers.Natural.Abstract.NOrder]
NOrderPropMod [module, in Coq.Numbers.Natural.Abstract.NAddOrder]
normalization_done [inductive, in Coq.Classes.Morphisms]
Normalizes [record, in Coq.Classes.Morphisms]
Normalizes [inductive, in Coq.Classes.Morphisms]
normalizes [projection, in Coq.Classes.Morphisms]
normalizes [constructor, in Coq.Classes.Morphisms]
not [definition, in Coq.Init.Logic]
Notations [library]
notT [definition, in Coq.Init.Logic_Type]
notzerop [definition, in Coq.Arith.Bool_nat]
notzerop_bool [definition, in Coq.Arith.Bool_nat]
not_all_ex_not [lemma, in Coq.Logic.Classical_Pred_Type]
not_all_ex_not [lemma, in Coq.Logic.Classical_Pred_Set]
not_all_not_ex [lemma, in Coq.Logic.Classical_Pred_Set]
not_all_not_ex [lemma, in Coq.Logic.Classical_Pred_Type]
not_and [lemma, in Coq.Logic.Decidable]
not_and_iff [lemma, in Coq.Logic.Decidable]
not_and_or [lemma, in Coq.Logic.Classical_Prop]
Not_b [definition, in Coq.Logic.Berardi]
not_Empty_Add [lemma, in Coq.Sets.Constructive_sets]
not_empty_Inhabited [lemma, in Coq.Sets.Classical_sets]
not_eq [lemma, in Coq.Arith.Compare_dec]
not_eq_false_beq [definition, in Coq.Bool.BoolEq]
not_eq_S [lemma, in Coq.Init.Peano]
not_eq_sym [abbreviation, in Coq.Arith.Compare]
not_even_and_odd [lemma, in Coq.Arith.Even]
not_ex_all_not [lemma, in Coq.Logic.Classical_Pred_Set]
not_ex_all_not [lemma, in Coq.Logic.Classical_Pred_Type]
not_ex_not_all [lemma, in Coq.Logic.Classical_Pred_Set]
not_ex_not_all [lemma, in Coq.Logic.Classical_Pred_Type]
not_false_iff [lemma, in Coq.Logic.Decidable]
not_false_is_true [lemma, in Coq.Bool.Bool]
not_ge [lemma, in Coq.Arith.Compare_dec]
not_gt [lemma, in Coq.Arith.Compare_dec]
not_has_fixpoint [lemma, in Coq.Logic.Berardi]
not_iff [lemma, in Coq.Logic.Decidable]
not_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
not_imp [lemma, in Coq.Logic.Decidable]
not_imply_elim [lemma, in Coq.Logic.Classical_Prop]
not_imply_elim2 [lemma, in Coq.Logic.Classical_Prop]
not_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
not_imp_iff [lemma, in Coq.Logic.Decidable]
not_imp_rev_iff [lemma, in Coq.Logic.Decidable]
not_included_empty_Inhabited [lemma, in Coq.Sets.Classical_sets]
not_injective_elim [lemma, in Coq.Sets.Image]
not_INR [lemma, in Coq.Reals.RIneq]
not_INR_O [abbreviation, in Coq.Reals.RIneq]
not_Isnil_cons [lemma, in Coq.Lists.TheoryList]
not_le [lemma, in Coq.Arith.Compare_dec]
not_le_minus_0 [lemma, in Coq.Arith.Minus]
not_lt [lemma, in Coq.Arith.Compare_dec]
not_nm_INR [abbreviation, in Coq.Reals.RIneq]
not_not [lemma, in Coq.Logic.Decidable]
not_not_archimedean [lemma, in Coq.Reals.Rlogic]
not_not_iff [lemma, in Coq.Logic.Decidable]
not_or [lemma, in Coq.Logic.Decidable]
not_or_and [lemma, in Coq.Logic.Classical_Prop]
not_or_iff [lemma, in Coq.Logic.Decidable]
not_O_INR [abbreviation, in Coq.Reals.RIneq]
not_O_IZR [abbreviation, in Coq.Reals.RIneq]
not_prime_divide [lemma, in Coq.ZArith.Znumtheory]
not_prime_0 [lemma, in Coq.ZArith.Znumtheory]
not_prime_1 [lemma, in Coq.ZArith.Znumtheory]
not_rel_prime_0 [lemma, in Coq.ZArith.Znumtheory]
not_Rlt [lemma, in Coq.Reals.SeqProp]
not_SIncl_empty [lemma, in Coq.Sets.Classical_sets]
not_true_iff [lemma, in Coq.Logic.Decidable]
not_true_is_false [lemma, in Coq.Bool.Bool]
not_Zeq [lemma, in Coq.ZArith.Zorder]
not_Zeq_inf [lemma, in Coq.ZArith.ZArith_dec]
not_0_INR [lemma, in Coq.Reals.RIneq]
not_0_IZR [lemma, in Coq.Reals.RIneq]
not_1_INR [lemma, in Coq.Reals.RIneq]
no_cond [definition, in Coq.Reals.Ranalysis1]
no_fixpoint_negb [lemma, in Coq.Bool.Bool]
Npdist [definition, in Coq.NArith.Ndist]
Npdist_comm [lemma, in Coq.NArith.Ndist]
Npdist_eq_1 [lemma, in Coq.NArith.Ndist]
Npdist_eq_2 [lemma, in Coq.NArith.Ndist]
Npdist_ultra [lemma, in Coq.NArith.Ndist]
NPeano [library]
NPeanoAxiomsMod [module, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZ [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZsucc [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZAxiomsMod.NZ0 [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZle [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_eq_cases [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_irrefl [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZlt_succ_r [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmax [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmax_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmax_r [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmin [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmin_l [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.NZOrdAxiomsMod.NZmin_r [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.pred_0 [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion [definition, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_succ [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_wd [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion_0 [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.succ_neq_0 [lemma, in Coq.Numbers.Natural.Peano.NPeano]
NPeanoSubPropMod [module, in Coq.Numbers.Natural.Peano.NPeano]
NPgeb [definition, in Coq.ZArith.ZOdiv_def]
NPgeb_correct [lemma, in Coq.ZArith.ZOdiv_def]
NPgeb_Zge [lemma, in Coq.ZArith.ZOdiv]
NPgeb_Zlt [lemma, in Coq.ZArith.ZOdiv]
Nplength [definition, in Coq.NArith.Ndist]
Nplength_first_one [lemma, in Coq.NArith.Ndist]
Nplength_infty [lemma, in Coq.NArith.Ndist]
Nplength_lb [lemma, in Coq.NArith.Ndist]
Nplength_one [lemma, in Coq.NArith.Ndist]
Nplength_ub [lemma, in Coq.NArith.Ndist]
Nplength_ultra [lemma, in Coq.NArith.Ndist]
Nplength_ultra_1 [lemma, in Coq.NArith.Ndist]
Nplength_zeros [lemma, in Coq.NArith.Ndist]
Nplus [definition, in Coq.NArith.BinNat]
Nplus_assoc [lemma, in Coq.NArith.BinNat]
Nplus_comm [lemma, in Coq.NArith.BinNat]
Nplus_reg_l [lemma, in Coq.NArith.BinNat]
Nplus_succ [lemma, in Coq.NArith.BinNat]
Nplus_0_l [lemma, in Coq.NArith.BinNat]
Nplus_0_r [lemma, in Coq.NArith.BinNat]
Npos [constructor, in Coq.NArith.BinNat]
Npred [definition, in Coq.NArith.BinNat]
Npred_succ [lemma, in Coq.NArith.BinNat]
nprod [definition, in Coq.Numbers.NaryFunctions]
nprod_of_list [definition, in Coq.Numbers.NaryFunctions]
nprod_to_list [definition, in Coq.Numbers.NaryFunctions]
NPropMod [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
Nrec [definition, in Coq.NArith.BinNat]
Nrect [definition, in Coq.NArith.BinNat]
Nrect_base [lemma, in Coq.NArith.BinNat]
Nrect_step [lemma, in Coq.NArith.BinNat]
Nrec_base [lemma, in Coq.NArith.BinNat]
Nrec_step [lemma, in Coq.NArith.BinNat]
Nsame_bit0 [lemma, in Coq.NArith.Ndigits]
nshiftl [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_above_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_n_0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftl_S_tail [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr [definition, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_above_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_n_0 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_predsize_0_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_size [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_S_tail [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr_0_propagates [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
NSig [library]
NSigNAxioms [library]
NSig_NAxioms [module, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.B [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.BS [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.B0 [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.B_holds [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.Induction [section, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.Induction.A [variable, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.Induction.AS [variable, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.Induction.A0 [variable, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.Induction.A_wd [variable, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZ [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZadd [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZadd_succ_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZadd_0_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZeq [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZeq_equiv [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZinduction [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZmul [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZmul_succ_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZmul_0_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZpred [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZpred_succ [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsub [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsub_succ_r [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsub_0_r [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZsucc [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.NZ0 [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZAxiomsMod.N_of_Z [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZle [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_eq_cases [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_irrefl [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZlt_succ_r [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmax [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmax_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmax_r [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmin [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmin_l [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.NZmin_r [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_compare_alt [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_le [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_lt [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_max [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.NZOrdAxiomsMod.spec_min [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.pred_0 [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion [definition, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_succ [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_wd [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NSig_NAxioms.recursion_0 [lemma, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
Nsize [definition, in Coq.NArith.Ndigits]
NSub [library]
NSubPropFunct [module, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_assoc [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_nz [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_eq_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.add_sub_swap [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.le_sub_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_pred_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_sub_distr_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.mul_sub_distr_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_add [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_add_distr [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_diag [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_gt [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_succ_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_wd [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_l [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_le [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_0_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.sub_1_r [lemma, in Coq.Numbers.Natural.Abstract.NSub]
Nsucc [definition, in Coq.NArith.BinNat]
Nsucc_inj [lemma, in Coq.NArith.BinNat]
Nsucc_0 [lemma, in Coq.NArith.BinNat]
Nth [lemma, in Coq.Lists.TheoryList]
nth [definition, in Coq.Lists.List]
ntheq_eqst [lemma, in Coq.Lists.Streams]
nth_default [definition, in Coq.Lists.List]
nth_error [definition, in Coq.Lists.List]
Nth_func [definition, in Coq.Lists.TheoryList]
nth_In [lemma, in Coq.Lists.List]
nth_indep [lemma, in Coq.Lists.List]
nth_in_or_default [lemma, in Coq.Lists.List]
nth_le [lemma, in Coq.Arith.Between]
nth_le_length [lemma, in Coq.Lists.TheoryList]
nth_lt_O [lemma, in Coq.Lists.TheoryList]
nth_O [constructor, in Coq.Arith.Between]
nth_ok [definition, in Coq.Lists.List]
nth_overflow [lemma, in Coq.Lists.List]
nth_S [constructor, in Coq.Arith.Between]
nth_spec [inductive, in Coq.Lists.TheoryList]
nth_spec_O [constructor, in Coq.Lists.TheoryList]
nth_spec_S [constructor, in Coq.Lists.TheoryList]
nth_S_cons [lemma, in Coq.Lists.List]
NType [module, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.add [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.compare [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.div_eucl [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.eq [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.eq_bool [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.gcd [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.le [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.lt [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.max [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.min [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.modulo [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.mul [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.of_N [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.one [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.power_pos [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.pred [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_add [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_compare [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_div_eucl [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_eq_bool [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_gcd [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_modulo [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_mul [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_of_N [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pos [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_power_pos [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pred [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_pred0 [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sqrt [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_square [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sub [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_sub0 [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_succ [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_0 [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.spec_1 [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sqrt [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.square [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.sub [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.succ [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.t [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.to_N [definition, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.to_Z [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.zero [axiom, in Coq.Numbers.Natural.SpecViaZ.NSig]
NType_ZType [module, in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.spec_Zabs_N [axiom, in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.spec_Z_of_N [axiom, in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Zabs_N [axiom, in Coq.Numbers.Rational.BigQ.QMake]
NType_ZType.Z_of_N [axiom, in Coq.Numbers.Rational.BigQ.QMake]
nu [definition, in Coq.Logic.Eqdep_dec]
null_derivative_loc [lemma, in Coq.Reals.MVT]
null_derivative_0 [lemma, in Coq.Reals.MVT]
null_derivative_1 [lemma, in Coq.Reals.MVT]
NumPrelude [library]
nuncurry [definition, in Coq.Numbers.NaryFunctions]
nu_constant [definition, in Coq.Logic.Eqdep_dec]
nu_inv [definition, in Coq.Logic.Eqdep_dec]
nu_left_inv [lemma, in Coq.Logic.Eqdep_dec]
Nxor [definition, in Coq.NArith.Ndigits]
Nxor_assoc [lemma, in Coq.NArith.Ndigits]
Nxor_bit0 [lemma, in Coq.NArith.Ndigits]
Nxor_BVxor [lemma, in Coq.NArith.Ndigits]
Nxor_comm [lemma, in Coq.NArith.Ndigits]
Nxor_div2 [lemma, in Coq.NArith.Ndigits]
Nxor_eq [lemma, in Coq.NArith.Ndigits]
Nxor_eq_false [lemma, in Coq.NArith.Ndec]
Nxor_eq_true [lemma, in Coq.NArith.Ndec]
Nxor_neutral_left [lemma, in Coq.NArith.Ndigits]
Nxor_neutral_right [lemma, in Coq.NArith.Ndigits]
Nxor_nilpotent [lemma, in Coq.NArith.Ndigits]
Nxor_semantics [lemma, in Coq.NArith.Ndigits]
Nxor_sem_1 [lemma, in Coq.NArith.Ndigits]
Nxor_sem_2 [lemma, in Coq.NArith.Ndigits]
Nxor_sem_3 [lemma, in Coq.NArith.Ndigits]
Nxor_sem_4 [lemma, in Coq.NArith.Ndigits]
Nxor_sem_5 [lemma, in Coq.NArith.Ndigits]
Nxor_sem_6 [lemma, in Coq.NArith.Ndigits]
NZAdd [library]
NZAddOrder [library]
NZAddOrderPropFunct [module, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_lt_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_le_mono_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_le_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_lt_mono_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_neg_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_nonneg [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonneg_pos [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_nonpos_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_cases [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_nonneg [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZadd_pos_pos [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZle_le_add_le [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZle_lt_add_lt [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_add_pos_l [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_add_pos_r [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropFunct.NZlt_le_add_lt [lemma, in Coq.Numbers.NatInt.NZAddOrder]
NZAddOrderPropMod [module, in Coq.Numbers.NatInt.NZMulOrder]
NZAddPropFunct [module, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_assoc [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_cancel_l [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_cancel_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_comm [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_shuffle1 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_shuffle2 [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_succ_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_0_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_1_l [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZadd_1_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropFunct.NZsub_1_r [lemma, in Coq.Numbers.NatInt.NZAdd]
NZAddPropMod [module, in Coq.Numbers.NatInt.NZMul]
NZAxioms [library]
NZAxiomsMod [module, in Coq.Numbers.Natural.Binary.NBinDefs]
NZAxiomsMod [module, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
NZAxiomsMod [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
NZAxiomsMod [module, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NZAxiomsMod [module, in Coq.Numbers.Natural.Peano.NPeano]
NZAxiomsMod [module, in Coq.Numbers.Integer.Binary.ZBinary]
NZAxiomsMod [module, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZ [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd_succ_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZadd_0_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZeq [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZeq_equiv [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZinduction [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul_succ_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZmul_0_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZpred [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZpred_succ [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub_succ_r [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsub_0_r [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZsucc [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.NZ0 [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.P [abbreviation, in Coq.Numbers.NatInt.NZAxioms]
NZAxiomsSig.S [abbreviation, in Coq.Numbers.NatInt.NZAxioms]
NZBase [library]
NZBasePropFunct [module, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.CentralInduction [section, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.CentralInduction.A [variable, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.CentralInduction.A_wd [variable, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZcentral_induction [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZE_stepl [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZneq_sym [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj_wd [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropFunct.NZsucc_inj_wd_neg [lemma, in Coq.Numbers.NatInt.NZBase]
NZBasePropMod [module, in Coq.Numbers.NatInt.NZAdd]
NZCyclic [library]
NZCyclicAxiomsMod [module, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.BS [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B0 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.B_holds [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_0 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.gt_wB_1 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction [section, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.AS [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A0 [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Induction.A_wd [variable, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZadd [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZadd_succ_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZadd_0_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZeq [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZeq_equiv [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZinduction [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZmul [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZmul_succ_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZmul_0_l [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZpred [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZpred_mod_wB [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZpred_succ [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsub [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsub_succ_r [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsub_0_r [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsucc [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZsucc_mod_wB [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ0 [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z_mod [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.P [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.S [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.wB [abbreviation, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Z_to_NZ [definition, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Z_to_NZ_0 [lemma, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZMul [library]
NZMulOrder [library]
NZMulOrderMod [module, in Coq.Numbers.Integer.Abstract.ZBase]
NZMulOrderMod [module, in Coq.Numbers.Natural.Abstract.NBase]
NZMulOrderPropFunct [module, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_mul_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_mul_0_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_mul_0_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZeq_square_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZlt_0_mul [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZlt_1_mul_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_cancel_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_cancel_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_id_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_id_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_neg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_neg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonneg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonpos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_nonpos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_pos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_le_mono_pos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_neg_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_neg_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_pos_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_mono_pos_r [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_lt_pred [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_neg_neg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_neg_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_pos_neg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_pos_pos [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZmul_2_mono_l [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZneq_mul_0 [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_le_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_le_simpl_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_lt_mono_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulOrderPropFunct.NZsquare_lt_simpl_nonneg [lemma, in Coq.Numbers.NatInt.NZMulOrder]
NZMulPropFunct [module, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_add_distr_l [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_add_distr_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_assoc [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_comm [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_succ_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_0_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_1_l [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropFunct.NZmul_1_r [lemma, in Coq.Numbers.NatInt.NZMul]
NZMulPropMod [module, in Coq.Numbers.NatInt.NZOrder]
NZOrdAxiomsMod [module, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
NZOrdAxiomsMod [module, in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NZOrdAxiomsMod [module, in Coq.Numbers.Natural.Binary.NBinDefs]
NZOrdAxiomsMod [module, in Coq.Numbers.Integer.Binary.ZBinary]
NZOrdAxiomsMod [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
NZOrdAxiomsMod [module, in Coq.Numbers.Natural.Abstract.NAxioms]
NZOrdAxiomsMod [module, in Coq.Numbers.Natural.Peano.NPeano]
NZOrdAxiomsMod [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
NZOrdAxiomsSig [module, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZle [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_eq_cases [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_irrefl [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZlt_succ_r [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmax_r [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin_l [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrdAxiomsSig.NZmin_r [axiom, in Coq.Numbers.NatInt.NZAxioms]
NZOrder [library]
NZOrderPropFunct [module, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.A' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.A' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.A [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.A_wd [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.Center [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.Center.LeftInduction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.Center.RightInduction [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Induction.Center.z [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.left_step [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.left_step' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.left_step'' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZAcc_gt_wd [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZAcc_lt_wd [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZA'A_left [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZA'A_right [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_dec [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZeq_le_incl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZgt_wf [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlbase [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZleft_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZleft_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_antisymm [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_dec [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ge_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_gt_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ind [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_le_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_lt_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_neq [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_ngt [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_refl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_stepl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_stepr [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZle_0_1 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZls'_ls'' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZls_ls' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_asymm [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_dec [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_dne [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_exists_pred [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_exists_pred_strong [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_ge_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_gt_cases [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_ind [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_le_incl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_le_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_lt_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_neq [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_nge [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_stepl [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_stepr [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_iter_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_succ_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_trans [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_trichotomy [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_wf [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_0_1 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZlt_1_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_diag_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZneq_succ_iter_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnle_gt [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnle_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_ge [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_succ_diag_l [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZnlt_succ_r [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction'_0 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZorder_induction_0 [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrbase [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZright_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZright_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrs'_rs'' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZrs_rs' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_left_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_left_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_right_induction [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZstrong_right_induction' [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZsucc_iter [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZsucc_le_mono [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.NZsucc_lt_mono [lemma, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Rgt [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.right_step [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.right_step' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.right_step'' [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.Rlt [definition, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.WF [section, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropFunct.WF.z [variable, in Coq.Numbers.NatInt.NZOrder]
NZOrderPropMod [module, in Coq.Numbers.NatInt.NZAddOrder]
Nzorn [lemma, in Coq.Reals.RiemannInt_SF]
N0 [constructor, in Coq.NArith.BinNat]
N0_less_1 [lemma, in Coq.NArith.Ndigits]
N0_less_2 [lemma, in Coq.NArith.Ndigits]
N2Bv [definition, in Coq.NArith.Ndigits]
N2Bv_Bv2N [lemma, in Coq.NArith.Ndigits]
N2Bv_gen [definition, in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen [lemma, in Coq.NArith.Ndigits]
N2Bv_N2Bv_gen_above [lemma, in Coq.NArith.Ndigits]
N_as_DT [module, in Coq.Logic.DecidableTypeEx]
N_as_OT [module, in Coq.FSets.OrderedTypeEx]
N_as_OT.compare [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.eq [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.eq_dec [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.eq_refl [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.eq_sym [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.eq_trans [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.lt [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.lt_not_eq [lemma, in Coq.FSets.OrderedTypeEx]
N_as_OT.lt_trans [definition, in Coq.FSets.OrderedTypeEx]
N_as_OT.t [definition, in Coq.FSets.OrderedTypeEx]
N_digits [definition, in Coq.ZArith.Zlogarithm]
N_div_mod_eq [lemma, in Coq.ZArith.ZOdiv]
N_ind_double [lemma, in Coq.NArith.BinNat]
N_of_div2 [lemma, in Coq.NArith.Nnat]
N_of_double [lemma, in Coq.NArith.Nnat]
N_of_double_plus_one [lemma, in Coq.NArith.Nnat]
N_of_max [lemma, in Coq.NArith.Nnat]
N_of_min [lemma, in Coq.NArith.Nnat]
N_of_minus [lemma, in Coq.NArith.Nnat]
N_of_mult [lemma, in Coq.NArith.Nnat]
N_of_nat [definition, in Coq.NArith.Nnat]
N_of_nat_compare [lemma, in Coq.NArith.Nnat]
N_of_nat_of_N [lemma, in Coq.NArith.Nnat]
N_of_plus [lemma, in Coq.NArith.Nnat]
N_of_S [lemma, in Coq.NArith.Nnat]
N_rec_double [lemma, in Coq.NArith.BinNat]
n_Sn [lemma, in Coq.Init.Peano]
n_SSn [lemma, in Coq.Arith.Plus]
n_SSSn [lemma, in Coq.Arith.Plus]
n_SSSSn [lemma, in Coq.Arith.Plus]



Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (13562 entries)
Instance Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (96 entries)
Projection Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (210 entries)
Record Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (71 entries)
Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (6947 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (306 entries)
Constructor Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (351 entries)
Inductive Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (182 entries)
Abbreviation Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (295 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (2870 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (286 entries)
Axiom Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (433 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1189 entries)
Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (326 entries)