N (definition)
NAbstract.level [in level]
napply_then_last [in napply_then_last]
napply_except_last [in napply_except_last]
napply_cst [in napply_cst]
napply_discard [in napply_discard]
NatOrder.leb [in leb]
NatOrder.t [in t]
Nat_as_OT.eq_refl [in eq_refl]
nat_iter [in nat_iter]
nat_lt_ge_bool [in nat_lt_ge_bool]
nat_gt_le_bool [in nat_gt_le_bool]
nat_compare [in nat_compare]
Nat_as_OT.t [in t]
nat_eq_bool [in nat_eq_bool]
Nat_as_OT.compare [in compare]
nat_of_P_gt_Gt_compare_complement_morphism [in nat_of_P_gt_Gt_compare_complement_morphism]
nat_ge_lt_bool [in nat_ge_lt_bool]
nat_le_gt_bool [in nat_le_gt_bool]
Nat_as_OT.eq_sym [in eq_sym]
Nat_as_OT.eq_trans [in eq_trans]
nat_po [in nat_po]
Nat_as_OT.eq_dec [in eq_dec]
nat_of_ascii [in nat_of_ascii]
nat_noteq_bool [in nat_noteq_bool]
Nat_as_OT.lt [in lt]
Nat_as_OT.eq [in eq]
nat_compare_alt [in nat_compare_alt]
Nat.add [in add]
Nat.compare [in compare]
Nat.compare_spec [in compare_spec]
Nat.div [in div]
Nat.divide [in divide]
Nat.div_mod [in div_mod]
Nat.div2 [in div2]
Nat.div2_spec [in div2_spec]
Nat.eq [in eq]
Nat.eqb [in eqb]
Nat.eqb_eq [in eqb_eq]
Nat.eq_dec [in eq_dec]
Nat.eq_equiv [in eq_equiv]
Nat.Even [in Even]
Nat.even [in even]
Nat.even_spec [in even_spec]
Nat.gcd [in gcd]
Nat.gcd_greatest [in gcd_greatest]
Nat.gcd_divide_r [in gcd_divide_r]
Nat.gcd_divide_l [in gcd_divide_l]
Nat.land [in land]
Nat.land_spec [in land_spec]
Nat.ldiff [in ldiff]
Nat.ldiff_spec [in ldiff_spec]
Nat.le [in le]
Nat.leb [in leb]
Nat.leb_le [in leb_le]
Nat.log2 [in log2]
Nat.log2_spec [in log2_spec]
Nat.log2_nonpos [in log2_nonpos]
Nat.lor [in lor]
Nat.lor_spec [in lor_spec]
Nat.lt [in lt]
Nat.ltb [in ltb]
Nat.ltb_lt [in ltb_lt]
Nat.lxor [in lxor]
Nat.lxor_spec [in lxor_spec]
Nat.max [in max]
Nat.max_r [in max_r]
Nat.max_l [in max_l]
Nat.min [in min]
Nat.min_r [in min_r]
Nat.min_l [in min_l]
Nat.modulo [in modulo]
Nat.mod_bound_pos [in mod_bound_pos]
Nat.mul [in mul]
Nat.odd [in odd]
Nat.Odd [in Odd]
Nat.odd_spec [in odd_spec]
Nat.one [in one]
Nat.pow [in pow]
Nat.pow_0_r [in pow_0_r]
Nat.pow_succ_r [in pow_succ_r]
Nat.pred [in pred]
Nat.recursion [in recursion]
Nat.shiftl [in shiftl]
Nat.shiftl_spec_low [in shiftl_spec_low]
Nat.shiftl_spec_high [in shiftl_spec_high]
Nat.shiftr [in shiftr]
Nat.shiftr_spec [in shiftr_spec]
Nat.sqrt [in sqrt]
Nat.sqrt_spec [in sqrt_spec]
Nat.square [in square]
Nat.square_spec [in square_spec]
Nat.sub [in sub]
Nat.succ [in succ]
Nat.t [in t]
Nat.testbit [in testbit]
Nat.testbit_even_0 [in testbit_even_0]
Nat.testbit_even_succ [in testbit_even_succ]
Nat.testbit_odd_0 [in testbit_odd_0]
Nat.testbit_odd_succ [in testbit_odd_succ]
Nat.two [in two]
Nat.zero [in zero]
NBitsProp.b2n [in b2n]
NBitsProp.clearbit [in clearbit]
NBitsProp.eqf [in eqf]
NBitsProp.lnot [in lnot]
NBitsProp.ones [in ones]
NBitsProp.setbit [in setbit]
Nbound [in Nbound]
ncurry [in ncurry]
NdefOpsProp.def_add [in def_add]
NdefOpsProp.def_mul [in def_mul]
NdefOpsProp.even [in even]
NdefOpsProp.half [in half]
NdefOpsProp.half_aux [in half_aux]
NdefOpsProp.if_zero [in if_zero]
NdefOpsProp.log [in log]
NdefOpsProp.ltb [in ltb]
NdefOpsProp.pow [in pow]
negb [in negb]
neighbourhood [in neighbourhood]
neq [in neq]
nequiv_decb [in nequiv_decb]
nequiv_decb [in nequiv_decb]
nequiv_dec [in nequiv_dec]
nequiv_dec [in nequiv_dec]
Neven [in Neven]
NewtonInt [in NewtonInt]
Newton_integrable [in Newton_integrable]
nfold [in nfold]
nfold_list [in nfold_list]
nfold_bis [in nfold_bis]
nfun [in nfun]
nfun_to_nfun [in nfun_to_nfun]
nfun_to_nfun_bis [in nfun_to_nfun_bis]
NGcdProp.Bezout [in Bezout]
NGcdProp.divide_1_r [in divide_1_r]
NGcdProp.divide_antisym [in divide_antisym]
NGcdProp.divide_gcd_iff' [in divide_gcd_iff']
NGcdProp.gcd_unique_alt' [in gcd_unique_alt']
NGcdProp.gcd_0_r [in gcd_0_r]
NGcdProp.gcd_0_l [in gcd_0_l]
NGcdProp.gcd_diag [in gcd_diag]
NGcdProp.gcd_unique' [in gcd_unique']
ni_le [in ni_le]
ni_min [in ni_min]
NLcmProp.lcm [in lcm]
Nleb [in Nleb]
Nless [in Nless]
Nless_aux [in Nless_aux]
NMulOrderProp.mul_eq_1 [in mul_eq_1]
Nodd [in Nodd]
NodepOfDep.add [in add]
NodepOfDep.Add [in Add]
NodepOfDep.cardinal [in cardinal]
NodepOfDep.choose [in choose]
NodepOfDep.compare [in compare]
NodepOfDep.diff [in diff]
NodepOfDep.elements [in elements]
NodepOfDep.elt [in elt]
NodepOfDep.empty [in empty]
NodepOfDep.Empty [in Empty]
NodepOfDep.eq [in eq]
NodepOfDep.equal [in equal]
NodepOfDep.Equal [in Equal]
NodepOfDep.eq_refl [in eq_refl]
NodepOfDep.eq_sym [in eq_sym]
NodepOfDep.eq_trans [in eq_trans]
NodepOfDep.eq_dec [in eq_dec]
NodepOfDep.Exists [in Exists]
NodepOfDep.exists_ [in exists_]
NodepOfDep.filter [in filter]
NodepOfDep.fold [in fold]
NodepOfDep.For_all [in For_all]
NodepOfDep.for_all [in for_all]
NodepOfDep.f_dec [in f_dec]
NodepOfDep.In [in In]
NodepOfDep.inter [in inter]
NodepOfDep.In_1 [in In_1]
NodepOfDep.is_empty [in is_empty]
NodepOfDep.lt [in lt]
NodepOfDep.lt_not_eq [in lt_not_eq]
NodepOfDep.lt_trans [in lt_trans]
NodepOfDep.max_elt [in max_elt]
NodepOfDep.mem [in mem]
NodepOfDep.min_elt [in min_elt]
NodepOfDep.partition [in partition]
NodepOfDep.remove [in remove]
NodepOfDep.singleton [in singleton]
NodepOfDep.Subset [in Subset]
NodepOfDep.subset [in subset]
NodepOfDep.t [in t]
NodepOfDep.union [in union]
Noetherian [in Noetherian]
not [in not]
notT [in notT]
notzerop [in notzerop]
notzerop_bool [in notzerop_bool]
not_eq_false_beq [in not_eq_false_beq]
Not_b [in Not_b]
no_cond [in no_cond]
Npdist [in Npdist]
Nplength [in Nplength]
NPowProp.pow_lt_mono [in pow_lt_mono]
NPowProp.pow_1_r [in pow_1_r]
NPowProp.pow_2_r [in pow_2_r]
nprod [in nprod]
nprod_of_list [in nprod_of_list]
nprod_to_list [in nprod_to_list]
nshiftl [in nshiftl]
nshiftr [in nshiftr]
NSqrtProp.sqrt_unique [in sqrt_unique]
NSqrtProp.sqrt_le_mono [in sqrt_le_mono]
NSqrtProp.sqrt_mul_below [in sqrt_mul_below]
NSqrtProp.sqrt_1 [in sqrt_1]
NSqrtProp.sqrt_0 [in sqrt_0]
NSqrtProp.sqrt_lt_cancel [in sqrt_lt_cancel]
NSqrtProp.sqrt_add_le [in sqrt_add_le]
NSqrtProp.sqrt_2 [in sqrt_2]
NSqrtProp.sqrt_lt_lin [in sqrt_lt_lin]
NStrongRecProp.strong_rec [in strong_rec]
NStrongRecProp.strong_rec0 [in strong_rec0]
NSubProp.le_alt [in le_alt]
NSubProp.lt_alt [in lt_alt]
nth [in nth]
nth [in nth]
nth_ok [in nth_ok]
nth_order [in nth_order]
nth_error [in nth_error]
nth_default [in nth_default]
NTypeIsNAxioms.divide [in divide]
NTypeIsNAxioms.Even [in Even]
NTypeIsNAxioms.N_of_Z [in N_of_Z]
NTypeIsNAxioms.Odd [in Odd]
NTypeIsNAxioms.recursion [in recursion]
NType.eq [in eq]
NType.le [in le]
NType.lt [in lt]
NType.to_N [in to_N]
nuncurry [in nuncurry]
NZCyclicAxiomsMod.add [in add]
NZCyclicAxiomsMod.eq [in eq]
NZCyclicAxiomsMod.mul [in mul]
NZCyclicAxiomsMod.one [in one]
NZCyclicAxiomsMod.pred [in pred]
NZCyclicAxiomsMod.sub [in sub]
NZCyclicAxiomsMod.succ [in succ]
NZCyclicAxiomsMod.t [in t]
NZCyclicAxiomsMod.two [in two]
NZCyclicAxiomsMod.zero [in zero]
NZDomainProp.initial [in initial]
NZGcdSpec.divide [in divide]
NZLog2UpProp.log2_up [in log2_up]
NZMulOrderProp.mul_eq_0_r [in mul_eq_0_r]
NZMulOrderProp.mul_eq_0_l [in mul_eq_0_l]
NZMulOrderProp.mul_eq_0 [in mul_eq_0]
NZOfNat.ofnat [in ofnat]
NZOrderProp.le_lteq [in le_lteq]
NZOrderProp.lt_compat [in lt_compat]
NZOrderProp.lt_total [in lt_total]
NZOrderProp.Private_OrderTac.Elts.le_lteq [in le_lteq]
NZOrderProp.Private_OrderTac.Elts.lt_compat [in lt_compat]
NZOrderProp.Private_OrderTac.Elts.lt_strorder [in lt_strorder]
NZOrderProp.Private_OrderTac.Elts.t [in t]
NZOrderProp.Private_OrderTac.Elts.le [in le]
NZOrderProp.Private_OrderTac.Elts.lt_total [in lt_total]
NZOrderProp.Private_OrderTac.Elts.eq_equiv [in eq_equiv]
NZOrderProp.Private_OrderTac.Elts.lt [in lt]
NZOrderProp.Private_OrderTac.Elts.eq [in eq]
NZParity.Even [in Even]
NZParity.Odd [in Odd]
NZSqrtUpProp.sqrt_up [in sqrt_up]
N_ind_double [in N_ind_double]
N_as_OT.eq_refl [in eq_refl]
N_of_ascii [in N_of_ascii]
N_as_OT.t [in t]
N_digits [in N_digits]
N_as_OT.compare [in compare]
N_of_digits [in N_of_digits]
N_as_OT.eq_sym [in eq_sym]
N_as_OT.lt_not_eq [in lt_not_eq]
N_as_OT.lt_trans [in lt_trans]
N_as_OT.eq_trans [in eq_trans]
N_as_OT.eq_dec [in eq_dec]
N_as_OT.lt [in lt]
N_rec_double [in N_rec_double]
N_as_OT.eq [in eq]
N.add [in add]
N.add_wd [in add_wd]
N.binary_ind [in binary_ind]
N.binary_rec [in binary_rec]
N.binary_rect [in binary_rect]
N.compare [in compare]
N.discr [in discr]
N.div [in div]
N.divide [in divide]
N.div_eucl [in div_eucl]
N.div_wd [in div_wd]
N.div_mod [in div_mod]
N.div2 [in div2]
N.div2_spec [in div2_spec]
N.double [in double]
N.eq [in eq]
N.eqb [in eqb]
N.eq_dec [in eq_dec]
N.eq_equiv [in eq_equiv]
N.Even [in Even]
N.even [in even]
N.gcd [in gcd]
N.ge [in ge]
N.ggcd [in ggcd]
N.gt [in gt]
N.iter [in iter]
N.land [in land]
N.ldiff [in ldiff]
N.le [in le]
N.leb [in leb]
N.log2 [in log2]
N.lor [in lor]
N.lt [in lt]
N.ltb [in ltb]
N.lt_wd [in lt_wd]
N.lxor [in lxor]
N.max [in max]
N.min [in min]
N.modulo [in modulo]
N.mod_wd [in mod_wd]
N.mul [in mul]
N.mul_wd [in mul_wd]
N.odd [in odd]
N.Odd [in Odd]
N.of_nat [in of_nat]
N.one [in one]
N.peano_ind [in peano_ind]
N.peano_rec [in peano_rec]
N.peano_rect [in peano_rect]
N.pos_div_eucl [in pos_div_eucl]
N.pow [in pow]
N.pow_wd [in pow_wd]
N.pred [in pred]
N.pred_0 [in pred_0]
N.pred_wd [in pred_wd]
N.recursion [in recursion]
N.shiftl [in shiftl]
N.shiftl_nat [in shiftl_nat]
N.shiftr [in shiftr]
N.shiftr_nat [in shiftr_nat]
N.size [in size]
N.size_nat [in size_nat]
N.sqrt [in sqrt]
N.sqrtrem [in sqrtrem]
N.square [in square]
N.sub [in sub]
N.sub_wd [in sub_wd]
N.succ [in succ]
N.succ_pos [in succ_pos]
N.succ_wd [in succ_wd]
N.succ_double [in succ_double]
N.t [in t]
N.testbit [in testbit]
N.testbit_nat [in testbit_nat]
N.testbit_wd [in testbit_wd]
N.to_nat [in to_nat]
N.two [in two]
N.zero [in zero]
N2Bv [in N2Bv]
N2Bv_gen [in N2Bv_gen]