N (definition)
napply_except_last [in Coq.Numbers.NaryFunctions]
napply_discard [in Coq.Numbers.NaryFunctions]
napply_then_last [in Coq.Numbers.NaryFunctions]
napply_cst [in Coq.Numbers.NaryFunctions]
nateq [in Coq.ring.LegacyArithRing]
NatHasMinMax.max [in Coq.Arith.MinMax]
NatHasMinMax.max_l [in Coq.Arith.MinMax]
NatHasMinMax.max_r [in Coq.Arith.MinMax]
NatHasMinMax.min [in Coq.Arith.MinMax]
NatHasMinMax.min_r [in Coq.Arith.MinMax]
NatHasMinMax.min_l [in Coq.Arith.MinMax]
NatOrder.leb [in Coq.Sorting.Mergesort]
NatOrder.t [in Coq.Sorting.Mergesort]
NatTheory [in Coq.ring.LegacyArithRing]
nat_le_gt_bool [in Coq.Arith.Bool_nat]
Nat_as_OT.eq_trans [in Coq.Structures.OrderedTypeEx]
Nat_as_OT.lt [in Coq.Arith.NatOrderedType]
Nat_as_OT.lt [in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq_refl [in Coq.Structures.OrderedTypeEx]
nat_of_P [in Coq.NArith.BinPos]
Nat_as_OT.eq [in Coq.Structures.OrderedTypeEx]
nat_ge_lt_bool [in Coq.Arith.Bool_nat]
Nat_as_OT.eq_sym [in Coq.Structures.OrderedTypeEx]
nat_of_bigint [in Coq.extraction.ExtrOcamlBigIntConv]
Nat_as_OT.compare [in Coq.Structures.OrderedTypeEx]
Nat_as_OT.t [in Coq.Structures.OrderedTypeEx]
Nat_as_OT.eq_dec [in Coq.Structures.OrderedTypeEx]
nat_of_int [in Coq.extraction.ExtrOcamlIntConv]
nat_lt_ge_bool [in Coq.Arith.Bool_nat]
Nat_as_UBE.eqb [in Coq.Arith.NatOrderedType]
nat_of_N [in Coq.NArith.Nnat]
Nat_as_UBE.eqb_eq [in Coq.Arith.NatOrderedType]
Nat_as_OT.compare_spec [in Coq.Arith.NatOrderedType]
nat_eq_bool [in Coq.Arith.Bool_nat]
nat_of_ascii [in Coq.Strings.Ascii]
Nat_as_UBE.eq [in Coq.Arith.NatOrderedType]
nat_noteq_bool [in Coq.Arith.Bool_nat]
nat_compare [in Coq.Arith.Compare_dec]
Nat_as_UBE.t [in Coq.Arith.NatOrderedType]
Nat_as_OT.compare [in Coq.Arith.NatOrderedType]
nat_gt_le_bool [in Coq.Arith.Bool_nat]
nat_po [in Coq.Sets.Integers]
Nat_as_OT.le_lteq [in Coq.Arith.NatOrderedType]
nat_compare_alt [in Coq.Arith.Compare_dec]
Nat_as_OT.le [in Coq.Arith.NatOrderedType]
NBasePropFunct.if_zero [in Coq.Numbers.Natural.Abstract.NBase]
NBinaryAxiomsMod.add [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.add_0_l [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.add_succ_l [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.eq [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.eq_equiv [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.le [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.lt [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.lt_eq_cases [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.lt_irrefl [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.max [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.min [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.mul [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.mul_succ_l [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.mul_0_l [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.pred [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.pred_succ [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.recursion [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.sub [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.sub_succ_r [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.sub_0_r [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.succ [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.t [in Coq.Numbers.Natural.Binary.NBinary]
NBinaryAxiomsMod.zero [in Coq.Numbers.Natural.Binary.NBinary]
Nbit [in Coq.NArith.Ndigits]
Nbit0 [in Coq.NArith.Ndigits]
Nbound [in Coq.Reals.RiemannInt_SF]
Ncompare [in Coq.NArith.BinNat]
ncurry [in Coq.Numbers.NaryFunctions]
NdefOpsPropFunct.def_add [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.def_mul [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.even [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.half [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.half_aux [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.log [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.ltb [in Coq.Numbers.Natural.Abstract.NDefOps]
NdefOpsPropFunct.pow [in Coq.Numbers.Natural.Abstract.NDefOps]
Ndiscr [in Coq.NArith.BinNat]
Ndiv [in Coq.ZArith.ZOdiv_def]
NDivMod.div [in Coq.Numbers.Natural.Peano.NPeano]
NDivMod.div_mod [in Coq.Numbers.Natural.Peano.NPeano]
NDivMod.modulo [in Coq.Numbers.Natural.Peano.NPeano]
NDivMod.mod_upper_bound [in Coq.Numbers.Natural.Peano.NPeano]
NDivPropFunct.ND.div [in Coq.Numbers.Natural.Abstract.NDiv]
NDivPropFunct.ND.div_mod [in Coq.Numbers.Natural.Abstract.NDiv]
NDivPropFunct.ND.div_wd [in Coq.Numbers.Natural.Abstract.NDiv]
NDivPropFunct.ND.modulo [in Coq.Numbers.Natural.Abstract.NDiv]
NDivPropFunct.ND.mod_wd [in Coq.Numbers.Natural.Abstract.NDiv]
Ndiv_eucl [in Coq.ZArith.ZOdiv_def]
Ndiv2 [in Coq.NArith.BinNat]
Ndouble [in Coq.NArith.BinNat]
Ndouble_plus_one [in Coq.NArith.BinNat]
negate [in Coq.micromega.ZMicromega]
negate [in Coq.micromega.RingMicromega]
negate_list [in Coq.micromega.CheckerMaker]
negb [in Coq.Init.Datatypes]
neighbourhood [in Coq.Reals.Rtopology]
neq [in Coq.ZArith.Znat]
Neq [in Coq.ring.LegacyNArithRing]
Neqb [in Coq.NArith.BinNat]
nequiv_decb [in Coq.Classes.SetoidDec]
nequiv_dec [in Coq.Classes.SetoidDec]
nequiv_decb [in Coq.Classes.EquivDec]
nequiv_dec [in Coq.Classes.EquivDec]
Neq_bool [in Coq.setoid_ring.InitialRing]
Neven [in Coq.NArith.Ndigits]
NewtonInt [in Coq.Reals.NewtonInt]
Newton_integrable [in Coq.Reals.NewtonInt]
nfold [in Coq.Numbers.NaryFunctions]
nfold_list [in Coq.Numbers.NaryFunctions]
nfold_bis [in Coq.Numbers.NaryFunctions]
NFormula [in Coq.micromega.RingMicromega]
nformula_plus_nformula [in Coq.micromega.RingMicromega]
nformula_times_nformula [in Coq.micromega.RingMicromega]
nformula_of_cutting_plane [in Coq.micromega.ZMicromega]
nfun [in Coq.Numbers.NaryFunctions]
nfun_to_nfun_bis [in Coq.Numbers.NaryFunctions]
nfun_to_nfun [in Coq.Numbers.NaryFunctions]
Nge [in Coq.NArith.BinNat]
Ngt [in Coq.NArith.BinNat]
NHasMinMax.max [in Coq.NArith.Nminmax]
NHasMinMax.max_r [in Coq.NArith.Nminmax]
NHasMinMax.max_l [in Coq.NArith.Nminmax]
NHasMinMax.min [in Coq.NArith.Nminmax]
NHasMinMax.min_r [in Coq.NArith.Nminmax]
NHasMinMax.min_l [in Coq.NArith.Nminmax]
Nind [in Coq.NArith.BinNat]
ni_min [in Coq.NArith.Ndist]
ni_le [in Coq.NArith.Ndist]
Nle [in Coq.NArith.BinNat]
Nleb [in Coq.NArith.Ndec]
Nless [in Coq.NArith.Ndigits]
Nless_aux [in Coq.NArith.Ndigits]
Nlt [in Coq.NArith.BinNat]
Nmax [in Coq.NArith.BinNat]
Nmin [in Coq.NArith.BinNat]
Nminus [in Coq.NArith.BinNat]
Nmin' [in Coq.NArith.Ndec]
Nmod [in Coq.ZArith.ZOdiv_def]
Nmult [in Coq.NArith.BinNat]
Nodd [in Coq.NArith.Ndigits]
node [in Coq.micromega.ZMicromega]
NodepOfDep.add [in Coq.FSets.FSetBridge]
NodepOfDep.Add [in Coq.FSets.FSetBridge]
NodepOfDep.cardinal [in Coq.FSets.FSetBridge]
NodepOfDep.choose [in Coq.FSets.FSetBridge]
NodepOfDep.compare [in Coq.FSets.FSetBridge]
NodepOfDep.diff [in Coq.FSets.FSetBridge]
NodepOfDep.elements [in Coq.FSets.FSetBridge]
NodepOfDep.elt [in Coq.FSets.FSetBridge]
NodepOfDep.empty [in Coq.FSets.FSetBridge]
NodepOfDep.Empty [in Coq.FSets.FSetBridge]
NodepOfDep.eq [in Coq.FSets.FSetBridge]
NodepOfDep.Equal [in Coq.FSets.FSetBridge]
NodepOfDep.equal [in Coq.FSets.FSetBridge]
NodepOfDep.eq_trans [in Coq.FSets.FSetBridge]
NodepOfDep.eq_refl [in Coq.FSets.FSetBridge]
NodepOfDep.eq_dec [in Coq.FSets.FSetBridge]
NodepOfDep.eq_sym [in Coq.FSets.FSetBridge]
NodepOfDep.Exists [in Coq.FSets.FSetBridge]
NodepOfDep.exists_ [in Coq.FSets.FSetBridge]
NodepOfDep.filter [in Coq.FSets.FSetBridge]
NodepOfDep.fold [in Coq.FSets.FSetBridge]
NodepOfDep.for_all [in Coq.FSets.FSetBridge]
NodepOfDep.For_all [in Coq.FSets.FSetBridge]
NodepOfDep.f_dec [in Coq.FSets.FSetBridge]
NodepOfDep.In [in Coq.FSets.FSetBridge]
NodepOfDep.inter [in Coq.FSets.FSetBridge]
NodepOfDep.In_1 [in Coq.FSets.FSetBridge]
NodepOfDep.is_empty [in Coq.FSets.FSetBridge]
NodepOfDep.lt [in Coq.FSets.FSetBridge]
NodepOfDep.lt_trans [in Coq.FSets.FSetBridge]
NodepOfDep.lt_not_eq [in Coq.FSets.FSetBridge]
NodepOfDep.max_elt [in Coq.FSets.FSetBridge]
NodepOfDep.mem [in Coq.FSets.FSetBridge]
NodepOfDep.min_elt [in Coq.FSets.FSetBridge]
NodepOfDep.partition [in Coq.FSets.FSetBridge]
NodepOfDep.remove [in Coq.FSets.FSetBridge]
NodepOfDep.singleton [in Coq.FSets.FSetBridge]
NodepOfDep.subset [in Coq.FSets.FSetBridge]
NodepOfDep.Subset [in Coq.FSets.FSetBridge]
NodepOfDep.t [in Coq.FSets.FSetBridge]
NodepOfDep.union [in Coq.FSets.FSetBridge]
Noetherian [in Coq.Sets.Relations_3]
Nopp [in Coq.setoid_ring.InitialRing]
norm [in Coq.micromega.ZMicromega]
norm [in Coq.nsatz.Nsatz]
norm [in Coq.micromega.RingMicromega]
normalise [in Coq.micromega.RingMicromega]
normalise [in Coq.micromega.ZMicromega]
normalise_list [in Coq.micromega.CheckerMaker]
norm_aux [in Coq.micromega.EnvRing]
norm_aux [in Coq.setoid_ring.Ring_polynom]
norm_subst [in Coq.micromega.EnvRing]
norm_subst [in Coq.setoid_ring.Ring_polynom]
not [in Coq.Init.Logic]
NotConstant [in Coq.setoid_ring.InitialRing]
notT [in Coq.Init.Logic_Type]
notzerop [in Coq.Arith.Bool_nat]
notzerop_bool [in Coq.Arith.Bool_nat]
Not_b [in Coq.Logic.Berardi]
not_eq_false_beq [in Coq.Bool.BoolEq]
no_cond [in Coq.Reals.Ranalysis1]
Npdist [in Coq.NArith.Ndist]
NPEadd [in Coq.setoid_ring.Field_theory]
NPeanoAxiomsMod.add [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.eq [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.eq_equiv [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.le [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.lt [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.max [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.min [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.mul [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.pred [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.recursion [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.sub [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.succ [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.t [in Coq.Numbers.Natural.Peano.NPeano]
NPeanoAxiomsMod.zero [in Coq.Numbers.Natural.Peano.NPeano]
NPEmul [in Coq.setoid_ring.Field_theory]
NPEopp [in Coq.setoid_ring.Field_theory]
NPEpow [in Coq.setoid_ring.Field_theory]
NPEsub [in Coq.setoid_ring.Field_theory]
NPgeb [in Coq.ZArith.ZOdiv_def]
Nplength [in Coq.NArith.Ndist]
Nplus [in Coq.NArith.BinNat]
Npred [in Coq.NArith.BinNat]
nprod [in Coq.Numbers.NaryFunctions]
nprod_to_list [in Coq.Numbers.NaryFunctions]
nprod_of_list [in Coq.Numbers.NaryFunctions]
Nrec [in Coq.NArith.BinNat]
Nrect [in Coq.NArith.BinNat]
nshiftl [in Coq.Numbers.Cyclic.Int31.Cyclic31]
nshiftr [in Coq.Numbers.Cyclic.Int31.Cyclic31]
Nsize [in Coq.NArith.Ndigits]
NStrongRecPropFunct.strong_rec [in Coq.Numbers.Natural.Abstract.NStrongRec]
NStrongRecPropFunct.strong_rec0 [in Coq.Numbers.Natural.Abstract.NStrongRec]
Nsub [in Coq.setoid_ring.InitialRing]
NSubPropFunct.le_alt [in Coq.Numbers.Natural.Abstract.NSub]
NSubPropFunct.lt_alt [in Coq.Numbers.Natural.Abstract.NSub]
Nsucc [in Coq.NArith.BinNat]
nth [in Coq.setoid_ring.BinList]
nth [in Coq.Lists.List]
nth [in Coq.micromega.Env]
NTheory [in Coq.ring.LegacyNArithRing]
nth_ok [in Coq.Lists.List]
nth_error [in Coq.Lists.List]
nth_default [in Coq.Lists.List]
Nth_func [in Coq.Lists.TheoryList]
NtoZ [in Coq.setoid_ring.Field_theory]
NTypeIsNAxioms.eqb [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NTypeIsNAxioms.N_of_Z [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NTypeIsNAxioms.recursion [in Coq.Numbers.Natural.SpecViaZ.NSigNAxioms]
NType.eq [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.le [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.lt [in Coq.Numbers.Natural.SpecViaZ.NSig]
NType.to_N [in Coq.Numbers.Natural.SpecViaZ.NSig]
nuncurry [in Coq.Numbers.NaryFunctions]
Nwadd [in Coq.setoid_ring.InitialRing]
Nwcons [in Coq.setoid_ring.InitialRing]
Nweq_bool [in Coq.setoid_ring.InitialRing]
NwI [in Coq.setoid_ring.InitialRing]
Nwmul [in Coq.setoid_ring.InitialRing]
NwO [in Coq.setoid_ring.InitialRing]
Nwopp [in Coq.setoid_ring.InitialRing]
Nword [in Coq.setoid_ring.InitialRing]
Nwscal [in Coq.setoid_ring.InitialRing]
Nwsub [in Coq.setoid_ring.InitialRing]
Nw_is0 [in Coq.setoid_ring.InitialRing]
Nxor [in Coq.NArith.Ndigits]
NZCyclicAxiomsMod.add [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.eq [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.mul [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.NZ_to_Z [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.pred [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.sub [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.succ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.t [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.zero [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZCyclicAxiomsMod.Z_to_NZ [in Coq.Numbers.Cyclic.Abstract.NZCyclic]
NZDomainProp.common_descendant [in Coq.Numbers.NatInt.NZDomain]
NZDomainProp.initial [in Coq.Numbers.NatInt.NZDomain]
NZOfNat.ofnat [in Coq.Numbers.NatInt.NZDomain]
NZOrderPropSig.le_lteq [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.lt_total [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.lt_compat [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.eq [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.eq_equiv [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.le [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.le_lteq [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.lt [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.lt_total [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.lt_compat [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.lt_strorder [in Coq.Numbers.NatInt.NZOrder]
NZOrderPropSig.OrderElts.t [in Coq.Numbers.NatInt.NZOrder]
n_of_int [in Coq.extraction.ExtrOcamlIntConv]
N_as_OT.eq_sym [in Coq.Structures.OrderedTypeEx]
N_as_OT.compare_spec [in Coq.NArith.NOrderedType]
N_as_UBE.eqb [in Coq.NArith.NOrderedType]
N_as_OT.eq [in Coq.Structures.OrderedTypeEx]
N_as_OT.lt_trans [in Coq.Structures.OrderedTypeEx]
N_eq [in Coq.setoid_ring.Field_theory]
N_as_UBE.eq [in Coq.NArith.NOrderedType]
N_as_OT.eq_dec [in Coq.Structures.OrderedTypeEx]
N_as_OT.lt_not_eq [in Coq.Structures.OrderedTypeEx]
N_of_Z [in Coq.setoid_ring.ZArithRing]
N_eq_dec [in Coq.NArith.BinNat]
N_as_OT.compare [in Coq.Structures.OrderedTypeEx]
N_as_UBE.t [in Coq.NArith.NOrderedType]
n_of_bigint [in Coq.extraction.ExtrOcamlBigIntConv]
N_of_nat [in Coq.NArith.Nnat]
N_as_OT.t [in Coq.Structures.OrderedTypeEx]
N_as_OT.eq_trans [in Coq.Structures.OrderedTypeEx]
n_of_Z [in Coq.micromega.ZMicromega]
N_of_digits [in Coq.Strings.Ascii]
N_as_OT.le_lteq [in Coq.NArith.NOrderedType]
N_as_OT.compare [in Coq.NArith.NOrderedType]
N_digits [in Coq.ZArith.Zlogarithm]
N_of_ascii [in Coq.Strings.Ascii]
N_as_UBE.eqb_eq [in Coq.NArith.NOrderedType]
N_as_OT.le [in Coq.NArith.NOrderedType]
N_as_OT.lt [in Coq.Structures.OrderedTypeEx]
N_as_OT.eq_refl [in Coq.Structures.OrderedTypeEx]
N_as_OT.lt [in Coq.NArith.NOrderedType]
N2Bv [in Coq.NArith.Ndigits]
N2Bv_gen [in Coq.NArith.Ndigits]