Coq.ZArith.Zwf

Global Index

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)

N

N [axiom, in Coq.Num.Definitions]
N [axiom, in Coq.Num.Params]
N [inductive, in Coq.NArith.BinNat]
NArith [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]
Nat_as_DT [module, in Coq.Logic.DecidableTypeEx]
Nat_as_OT [module, 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_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_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]
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_eq [lemma, in Coq.NArith.BinNat]
Ncompare_Neqb [lemma, in Coq.NArith.Ndec]
Ncompare_refl [lemma, in Coq.NArith.BinNat]
Ndec [library]
Ndigits [library]
Ndiscr [definition, in Coq.NArith.BinNat]
Ndist [library]
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]
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_monotonic [lemma, in Coq.IntMap.Lsort]
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]
Ndouble_plus_one_monotonic [lemma, in Coq.IntMap.Lsort]
necons [constructor, in Coq.Setoids.Setoid]
negative_derivative [lemma, in Coq.Reals.MVT]
negb [definition, in Coq.Bool.Bool]
negb_andb [lemma, 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 [inductive, in Coq.Reals.RIneq]
neg_cos [lemma, in Coq.Reals.Rtrigo]
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]
nelistT [inductive, in Coq.Setoids.Setoid]
neq [definition, in Coq.ZArith.Znat]
neq [axiom, in Coq.Num.NeqParams]
neq [definition, in Coq.Num.Definitions]
neq [definition, in Coq.Num.NeqDef]
NeqAxioms [library]
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]
NeqDef [library]
NeqParams [library]
NeqProps [library]
neq_antirefl [lemma, in Coq.Num.NeqProps]
neq_eq_compat [lemma, in Coq.Num.NeqProps]
neq_not_eq [lemma, in Coq.Num.NeqProps]
neq_not_eq_y_x [lemma, in Coq.Num.NeqProps]
neq_not_neq_trans [axiom, in Coq.Num.NeqAxioms]
neq_not_neq_trans [lemma, in Coq.Num.NeqDef]
neq_O_lt [lemma, in Coq.Arith.Lt]
neq_sym [axiom, in Coq.Num.NeqAxioms]
neq_sym [lemma, in Coq.Num.NeqDef]
neq_x_Sx [lemma, in Coq.Num.LtProps]
neq_0_1 [lemma, in Coq.Num.LtProps]
Neven [definition, in Coq.NArith.Ndigits]
Neven_not_double_plus_one [lemma, in Coq.NArith.Ndec]
Newman [lemma, in Coq.Sets.Relations_3_facts]
Newman [lemma, in Coq.Relations.Newman]
Newman [library]
newMap [definition, in Coq.IntMap.Map]
newMap_semantics [lemma, in Coq.IntMap.Map]
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]
ni [constructor, in Coq.NArith.Ndist]
nil [constructor, in Coq.Lists.List]
nil [constructor, in Coq.Reals.RList]
nil [constructor, in Coq.Lists.MonoList]
nil_cons [lemma, in Coq.Lists.MonoList]
nil_cons [lemma, in Coq.Lists.List]
nil_is_heap [constructor, in Coq.Sorting.Heap]
nil_leA [constructor, in Coq.Sorting.Sorting]
nil_sort [constructor, in Coq.Sorting.Sorting]
Nind [lemma, in Coq.NArith.BinNat]
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.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]
Nle_antisym [lemma, in Coq.NArith.Ndec]
Nle_double_mono [lemma, in Coq.NArith.Ndec]
Nle_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nle_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nle_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nle_lt_trans [lemma, in Coq.NArith.Ndec]
Nle_Ncompare [lemma, in Coq.NArith.Ndec]
Nle_refl [lemma, in Coq.NArith.Ndec]
Nle_trans [lemma, in Coq.NArith.Ndec]
Nlt_double_mono [lemma, in Coq.NArith.Ndec]
Nlt_double_mono_conv [lemma, in Coq.NArith.Ndec]
Nlt_double_plus_one_mono [lemma, in Coq.NArith.Ndec]
Nlt_double_plus_one_mono_conv [lemma, in Coq.NArith.Ndec]
Nlt_le_trans [lemma, in Coq.NArith.Ndec]
Nlt_le_weak [lemma, in Coq.NArith.Ndec]
Nlt_trans [lemma, in Coq.NArith.Ndec]
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]
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_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]
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.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.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_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_eqlistA_permut [lemma, in Coq.Sorting.PermutSetoid]
NoDupA_nil [constructor, in Coq.Lists.SetoidList]
NoDupA_rev [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 [inductive, in Coq.Sets.Relations_3]
noetherian [definition, in Coq.Relations.Newman]
Noetherian [definition, in Coq.Sets.Relations_3]
Noetherian_contains_Noetherian [lemma, in Coq.Sets.Relations_3_facts]
None [constructor, in Coq.Init.Datatypes]
nonnegreal [inductive, in Coq.Reals.RIneq]
nonneg_derivative_0 [lemma, in Coq.Reals.Ranalysis1]
nonneg_derivative_1 [lemma, in Coq.Reals.MVT]
nonposreal [inductive, in Coq.Reals.RIneq]
nonpos_derivative_0 [lemma, in Coq.Reals.MVT]
nonpos_derivative_1 [lemma, in Coq.Reals.MVT]
nonzeroreal [inductive, 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]
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_Set]
not_all_ex_not [lemma, in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [lemma, in Coq.Logic.Classical_Pred_Type]
not_all_not_ex [lemma, in Coq.Logic.Classical_Pred_Set]
not_and [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_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_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_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_included_empty_Inhabited [lemma, in Coq.Sets.Classical_sets]
not_injective_elim [lemma, in Coq.Sets.Image]
not_INR_O [lemma, in Coq.Reals.RIneq]
not_Isnil_cons [lemma, in Coq.Lists.TheoryList]
not_le [lemma, in Coq.Arith.Compare_dec]
not_le_gt [axiom, in Coq.Num.GtAxioms]
not_le_minus_0 [lemma, in Coq.Arith.Minus]
not_lt [lemma, in Coq.Arith.Compare_dec]
not_lt_ge [axiom, in Coq.Num.GeAxioms]
not_neq_neq_trans [lemma, in Coq.Num.NeqProps]
not_nm_INR [lemma, in Coq.Reals.RIneq]
not_not [lemma, in Coq.Logic.Decidable]
not_or [lemma, in Coq.Logic.Decidable]
not_or_and [lemma, in Coq.Logic.Classical_Prop]
not_O_INR [lemma, in Coq.Reals.RIneq]
not_O_IZR [lemma, in Coq.Reals.RIneq]
not_Rlt [lemma, in Coq.Reals.SeqProp]
not_SIncl_empty [lemma, in Coq.Sets.Classical_sets]
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_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]
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]
Nsame_bit0 [lemma, in Coq.NArith.Ndigits]
Nsize [definition, in Coq.NArith.Ndigits]
Nsucc [definition, in Coq.NArith.BinNat]
Nsucc_inj [lemma, in Coq.NArith.BinNat]
NSyntax [library]
nth [definition, in Coq.Lists.List]
Nth [lemma, in Coq.Lists.TheoryList]
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]
null_derivative_loc [lemma, in Coq.Reals.MVT]
null_derivative_0 [lemma, in Coq.Reals.MVT]
null_derivative_1 [lemma, in Coq.Reals.MVT]
NUsualOrderedType [module, in Coq.FSets.FMapIntMap]
NUsualOrderedType.compare [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.eq [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.eq_refl [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.eq_sym [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.eq_trans [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.lt [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.lt_not_eq [lemma, in Coq.FSets.FMapIntMap]
NUsualOrderedType.lt_trans [definition, in Coq.FSets.FMapIntMap]
NUsualOrderedType.t [definition, in Coq.FSets.FMapIntMap]
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]
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_digits [definition, in Coq.ZArith.Zlogarithm]
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_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

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)