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 _ other (18816 entries)
Notation 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 _ other (644 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 _ other (708 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 _ other (1456 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 _ other (407 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 _ other (8932 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 _ other (422 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 _ other (699 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 _ other (209 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 _ other (203 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 _ other (550 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 _ other (338 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 _ other (1235 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 _ other (2946 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 _ other (67 entries)

N

N [module, in N]
N [inductive, in N]
N [module, in N]
N [module, in N]
NAbstract [module, in NAbstract]
NAbstract.destr_t [axiom, in destr_t]
NAbstract.digits_dom_op [axiom, in digits_dom_op]
NAbstract.dom_t [axiom, in dom_t]
NAbstract.dom_op [instance, in dom_op]
NAbstract.dom_spec [instance, in dom_spec]
NAbstract.iter_t [axiom, in iter_t]
NAbstract.iter_mk_t [axiom, in iter_mk_t]
NAbstract.level [definition, in level]
NAbstract.mk_t_S_level [axiom, in mk_t_S_level]
NAbstract.Mk_t [constructor, in Mk_t]
NAbstract.mk_t [axiom, in mk_t]
NAbstract.mk_t_S [axiom, in mk_t_S]
NAbstract.reduce [axiom, in reduce]
NAbstract.same_level [axiom, in same_level]
NAbstract.spec_mk_t [axiom, in spec_mk_t]
NAbstract.spec_same_level_dep [axiom, in spec_same_level_dep]
NAbstract.spec_mk_t_S [axiom, in spec_mk_t_S]
NAbstract.spec_reduce [axiom, in spec_reduce]
NAbstract.t [axiom, in t]
NAbstract.to_Z [axiom, in to_Z]
NAbstract.View_t [inductive, in View_t]
[ _ ] [notation, in ::'['_x_']']
NAdd [library]
NAddOrder [library]
NAddOrderProp [module, in NAddOrderProp]
NAddOrderProp.add_pos_l [lemma, in add_pos_l]
NAddOrderProp.add_pos_r [lemma, in add_pos_r]
NAddOrderProp.le_add_r [lemma, in le_add_r]
NAddOrderProp.lt_lt_add_l [lemma, in lt_lt_add_l]
NAddOrderProp.lt_lt_add_r [lemma, in lt_lt_add_r]
NAddProp [module, in NAddProp]
NAddProp.add_pred_r [lemma, in add_pred_r]
NAddProp.add_pred_l [lemma, in add_pred_l]
NAddProp.eq_add_1 [lemma, in eq_add_1]
NAddProp.eq_add_succ [lemma, in eq_add_succ]
NAddProp.eq_add_0 [lemma, in eq_add_0]
NAddProp.succ_add_discr [lemma, in succ_add_discr]
Nand_semantics [lemma, in Nand_semantics]
Nand_BVand [lemma, in Nand_BVand]
napply_then_last [definition, in napply_then_last]
napply_except_last [definition, in napply_except_last]
napply_cst [definition, in napply_cst]
napply_discard [definition, in napply_discard]
NArith [library]
NaryFunctions [library]
Nat [module, in Nat]
nat [inductive, in nat]
natinf [inductive, in natinf]
natlike_rec2 [lemma, in natlike_rec2]
natlike_rec [lemma, in natlike_rec]
natlike_ind [lemma, in natlike_ind]
natlike_rec3 [lemma, in natlike_rec3]
NatOrder [module, in NatOrder]
NatOrder.leb [definition, in leb]
NatOrder.leb_total [lemma, in leb_total]
NatOrder.t [definition, in t]
_ <=? _ [notation, in ::x_'<=?'_x]
NatSeq [section, in NatSeq]
NatSort [module, in NatSort]
Nat_as_OT [module, in Nat_as_OT]
Nat_as_OT [module, in Nat_as_OT]
nat_of_P_gt_Gt_compare_morphism [lemma, in nat_of_P_gt_Gt_compare_morphism]
nat_of_P_lt_Lt_compare_complement_morphism [lemma, in nat_of_P_lt_Lt_compare_complement_morphism]
nat_of_Nplus [abbreviation, in nat_of_Nplus]
nat_of_P_inj_iff [abbreviation, in nat_of_P_inj_iff]
nat_iter_wd [instance, in nat_iter_wd]
Nat_as_OT.eq_refl [definition, in eq_refl]
nat_compare_gt [lemma, in nat_compare_gt]
nat_iter_succ_r [lemma, in nat_iter_succ_r]
nat_iter_plus [lemma, in nat_iter_plus]
nat_iter [definition, in nat_iter]
nat_of_P_of_succ_nat [abbreviation, in nat_of_P_of_succ_nat]
nat_of_P_o_P_of_succ_nat_eq_succ [abbreviation, in nat_of_P_o_P_of_succ_nat_eq_succ]
nat_compare_lt [lemma, in nat_compare_lt]
nat_of_P_is_S [abbreviation, in nat_of_P_is_S]
nat_of_P_mult_morphism [abbreviation, in nat_of_P_mult_morphism]
nat_compare_Gt_gt [lemma, in nat_compare_Gt_gt]
nat_lt_ge_bool [definition, in nat_lt_ge_bool]
nat_gt_le_bool [definition, in nat_gt_le_bool]
nat_total_order [lemma, in nat_total_order]
nat_compare [definition, in nat_compare]
Nat_as_OT.t [definition, in t]
nat_of_P_plus_morphism [abbreviation, in nat_of_P_plus_morphism]
nat_eq_bool [definition, in nat_eq_bool]
nat_compare_eq_iff [lemma, in nat_compare_eq_iff]
nat_of_Ndiv2 [abbreviation, in nat_of_Ndiv2]
nat_of_P_xI [abbreviation, in nat_of_P_xI]
Nat_as_OT.compare [definition, in compare]
nat_of_P [abbreviation, in nat_of_P]
nat_of_P_xH [abbreviation, in nat_of_P_xH]
nat_of_P_gt_Gt_compare_complement_morphism [definition, in nat_of_P_gt_Gt_compare_complement_morphism]
nat_ge_lt_bool [definition, in nat_ge_lt_bool]
nat_of_P_lt_Lt_compare_morphism [lemma, in nat_of_P_lt_Lt_compare_morphism]
nat_ascii_embedding [lemma, in nat_ascii_embedding]
nat_of_Ndouble_plus_one [abbreviation, in nat_of_Ndouble_plus_one]
nat_double_ind [lemma, in nat_double_ind]
nat_le_gt_bool [definition, in nat_le_gt_bool]
nat_compare_ge [lemma, in nat_compare_ge]
nat_of_P_succ_morphism [abbreviation, in nat_of_P_succ_morphism]
nat_compare_Lt_lt [lemma, in nat_compare_Lt_lt]
Nat_as_OT.eq_sym [definition, in eq_sym]
nat_of_N_of_nat [abbreviation, in nat_of_N_of_nat]
nat_of_P_xO [abbreviation, in nat_of_P_xO]
Nat_as_OT.lt_not_eq [lemma, in lt_not_eq]
nat_of_Nmax [abbreviation, in nat_of_Nmax]
Nat_as_OT.lt_trans [lemma, in lt_trans]
nat_case [lemma, in nat_case]
Nat_as_OT.eq_trans [definition, in eq_trans]
nat_po [definition, in nat_po]
nat_compare_spec [lemma, in nat_compare_spec]
nat_compare_equiv [lemma, in nat_compare_equiv]
nat_compare_eq [lemma, in nat_compare_eq]
Nat_as_OT.eq_dec [definition, in eq_dec]
nat_of_N [abbreviation, in nat_of_N]
nat_of_Ncompare [abbreviation, in nat_of_Ncompare]
nat_eq_eqdec [instance, in nat_eq_eqdec]
nat_eq_eqdec [instance, in nat_eq_eqdec]
nat_of_P_minus_morphism [lemma, in nat_of_P_minus_morphism]
nat_of_Nmin [abbreviation, in nat_of_Nmin]
nat_of_Nsucc [abbreviation, in nat_of_Nsucc]
Nat_as_DT [module, in Nat_as_DT]
Nat_as_DT [module, in Nat_as_DT]
nat_of_ascii [definition, in nat_of_ascii]
nat_of_Ndouble [abbreviation, in nat_of_Ndouble]
nat_N_Z [lemma, in nat_N_Z]
nat_noteq_bool [definition, in nat_noteq_bool]
Nat_as_OT.lt [definition, in lt]
nat_of_P_pos [abbreviation, in nat_of_P_pos]
nat_of_P_inj [abbreviation, in nat_of_P_inj]
nat_compare_S [lemma, in nat_compare_S]
nat_compare_le [lemma, in nat_compare_le]
nat_of_N_inj [abbreviation, in nat_of_N_inj]
nat_iter_invariant [lemma, in nat_iter_invariant]
nat_of_Nminus [abbreviation, in nat_of_Nminus]
Nat_as_OT.eq [definition, in eq]
nat_compare_alt [definition, in nat_compare_alt]
nat_of_Npred [abbreviation, in nat_of_Npred]
nat_of_P_compare_morphism [abbreviation, in nat_of_P_compare_morphism]
nat_of_Nmult [abbreviation, in nat_of_Nmult]
Nat.add [definition, in add]
Nat.add_succ_l [lemma, in add_succ_l]
Nat.add_0_l [lemma, in add_0_l]
Nat.add_wd [instance, in add_wd]
Nat.bi_induction [lemma, in bi_induction]
Nat.compare [definition, in compare]
Nat.compare_spec [definition, in compare_spec]
Nat.div [definition, in div]
Nat.divide [definition, in divide]
Nat.div_wd [instance, in div_wd]
Nat.div_mod [definition, in div_mod]
Nat.div2 [definition, in div2]
Nat.div2_spec [definition, in div2_spec]
Nat.eq [definition, in eq]
Nat.eqb [definition, in eqb]
Nat.eqb_eq [definition, in eqb_eq]
Nat.eq_dec [definition, in eq_dec]
Nat.eq_equiv [definition, in eq_equiv]
Nat.Even [definition, in Even]
Nat.even [definition, in even]
Nat.even_spec [definition, in even_spec]
Nat.gcd [definition, in gcd]
Nat.gcd_nonneg [lemma, in gcd_nonneg]
Nat.gcd_greatest [definition, in gcd_greatest]
Nat.gcd_divide_r [definition, in gcd_divide_r]
Nat.gcd_divide_l [definition, in gcd_divide_l]
Nat.land [definition, in land]
Nat.land_spec [definition, in land_spec]
Nat.ldiff [definition, in ldiff]
Nat.ldiff_spec [definition, in ldiff_spec]
Nat.le [definition, in le]
Nat.leb [definition, in leb]
Nat.leb_le [definition, in leb_le]
Nat.log2 [definition, in log2]
Nat.log2_spec [definition, in log2_spec]
Nat.log2_nonpos [definition, in log2_nonpos]
Nat.lor [definition, in lor]
Nat.lor_spec [definition, in lor_spec]
Nat.lt [definition, in lt]
Nat.ltb [definition, in ltb]
Nat.ltb_lt [definition, in ltb_lt]
Nat.lt_irrefl [lemma, in lt_irrefl]
Nat.lt_eq_cases [lemma, in lt_eq_cases]
Nat.lt_succ_r [lemma, in lt_succ_r]
Nat.lt_wd [instance, in lt_wd]
Nat.lxor [definition, in lxor]
Nat.lxor_spec [definition, in lxor_spec]
Nat.max [definition, in max]
Nat.max_r [definition, in max_r]
Nat.max_l [definition, in max_l]
Nat.min [definition, in min]
Nat.min_r [definition, in min_r]
Nat.min_l [definition, in min_l]
Nat.modulo [definition, in modulo]
Nat.mod_bound_pos [definition, in mod_bound_pos]
Nat.mod_wd [instance, in mod_wd]
Nat.mul [definition, in mul]
Nat.mul_succ_l [lemma, in mul_succ_l]
Nat.mul_0_l [lemma, in mul_0_l]
Nat.mul_wd [instance, in mul_wd]
Nat.odd [definition, in odd]
Nat.Odd [definition, in Odd]
Nat.odd_spec [definition, in odd_spec]
Nat.one [definition, in one]
Nat.one_succ [lemma, in one_succ]
Nat.pow [definition, in pow]
Nat.pow_wd [instance, in pow_wd]
Nat.pow_0_r [definition, in pow_0_r]
Nat.pow_succ_r [definition, in pow_succ_r]
Nat.pow_neg_r [lemma, in pow_neg_r]
Nat.pred [definition, in pred]
Nat.pred_succ [lemma, in pred_succ]
Nat.pred_0 [lemma, in pred_0]
Nat.pred_wd [instance, in pred_wd]
Nat.recursion [definition, in recursion]
Nat.recursion_wd [instance, in recursion_wd]
Nat.recursion_0 [lemma, in recursion_0]
Nat.recursion_succ [lemma, in recursion_succ]
Nat.shiftl [definition, in shiftl]
Nat.shiftl_spec_low [definition, in shiftl_spec_low]
Nat.shiftl_spec_high [definition, in shiftl_spec_high]
Nat.shiftr [definition, in shiftr]
Nat.shiftr_spec [definition, in shiftr_spec]
Nat.sqrt [definition, in sqrt]
Nat.sqrt_spec [definition, in sqrt_spec]
Nat.sqrt_neg [lemma, in sqrt_neg]
Nat.square [definition, in square]
Nat.square_spec [definition, in square_spec]
Nat.sub [definition, in sub]
Nat.sub_wd [instance, in sub_wd]
Nat.sub_succ_r [lemma, in sub_succ_r]
Nat.sub_0_r [lemma, in sub_0_r]
Nat.succ [definition, in succ]
Nat.succ_wd [instance, in succ_wd]
Nat.t [definition, in t]
Nat.testbit [definition, in testbit]
Nat.testbit_even_0 [definition, in testbit_even_0]
Nat.testbit_neg_r [lemma, in testbit_neg_r]
Nat.testbit_even_succ [definition, in testbit_even_succ]
Nat.testbit_odd_0 [definition, in testbit_odd_0]
Nat.testbit_odd_succ [definition, in testbit_odd_succ]
Nat.testbit_wd [instance, in testbit_wd]
Nat.two [definition, in two]
Nat.two_succ [lemma, in two_succ]
Nat.zero [definition, in zero]
Nat2N [module, in Nat2N]
Nat2N.id [lemma, in id]
Nat2N.inj [lemma, in inj]
Nat2N.inj_max [lemma, in inj_max]
Nat2N.inj_succ_double [lemma, in inj_succ_double]
Nat2N.inj_mul [lemma, in inj_mul]
Nat2N.inj_double [lemma, in inj_double]
Nat2N.inj_iff [lemma, in inj_iff]
Nat2N.inj_iter [lemma, in inj_iter]
Nat2N.inj_add [lemma, in inj_add]
Nat2N.inj_div2 [lemma, in inj_div2]
Nat2N.inj_compare [lemma, in inj_compare]
Nat2N.inj_sub [lemma, in inj_sub]
Nat2N.inj_min [lemma, in inj_min]
Nat2N.inj_pred [lemma, in inj_pred]
Nat2N.inj_succ [lemma, in inj_succ]
Nat2Pos [module, in Nat2Pos]
Nat2Pos.id [lemma, in id]
Nat2Pos.id_max [lemma, in id_max]
Nat2Pos.inj [lemma, in inj]
Nat2Pos.inj_max [lemma, in inj_max]
Nat2Pos.inj_mul [lemma, in inj_mul]
Nat2Pos.inj_iff [lemma, in inj_iff]
Nat2Pos.inj_add [lemma, in inj_add]
Nat2Pos.inj_compare [lemma, in inj_compare]
Nat2Pos.inj_sub [lemma, in inj_sub]
Nat2Pos.inj_min [lemma, in inj_min]
Nat2Pos.inj_pred [lemma, in inj_pred]
Nat2Pos.inj_succ [lemma, in inj_succ]
Nat2Z [module, in Nat2Z]
Nat2Z.id [lemma, in id]
Nat2Z.inj [lemma, in inj]
Nat2Z.inj_max [lemma, in inj_max]
Nat2Z.inj_lt [lemma, in inj_lt]
Nat2Z.inj_abs_nat [lemma, in inj_abs_nat]
Nat2Z.inj_mul [lemma, in inj_mul]
Nat2Z.inj_pred_max [lemma, in inj_pred_max]
Nat2Z.inj_iff [lemma, in inj_iff]
Nat2Z.inj_0 [lemma, in inj_0]
Nat2Z.inj_add [lemma, in inj_add]
Nat2Z.inj_ge [lemma, in inj_ge]
Nat2Z.inj_compare [lemma, in inj_compare]
Nat2Z.inj_sub [lemma, in inj_sub]
Nat2Z.inj_min [lemma, in inj_min]
Nat2Z.inj_le [lemma, in inj_le]
Nat2Z.inj_pred [lemma, in inj_pred]
Nat2Z.inj_succ [lemma, in inj_succ]
Nat2Z.inj_sub_max [lemma, in inj_sub_max]
Nat2Z.inj_gt [lemma, in inj_gt]
Nat2Z.is_nonneg [lemma, in is_nonneg]
NAxiom [module, in NAxiom]
NAxioms [library]
NAxiomsFullSig [module, in NAxiomsFullSig]
NAxiomsFullSig' [module, in NAxiomsFullSig']
NAxiomsMiniSig [module, in NAxiomsMiniSig]
NAxiomsMiniSig' [module, in NAxiomsMiniSig']
NAxiomsRec [module, in NAxiomsRec]
NAxiomsRecSig [module, in NAxiomsRecSig]
NAxiomsRecSig' [module, in NAxiomsRecSig']
NAxiomsRec.recursion [axiom, in recursion]
NAxiomsRec.recursion_wd [instance, in recursion_wd]
NAxiomsRec.recursion_0 [axiom, in recursion_0]
NAxiomsRec.recursion_succ [axiom, in recursion_succ]
NAxiomsSig [module, in NAxiomsSig]
NAxiomsSig' [module, in NAxiomsSig']
NAxiom.pred_0 [axiom, in pred_0]
NBase [library]
NBaseProp [module, in NBaseProp]
NBaseProp.case_analysis [lemma, in case_analysis]
NBaseProp.DoubleInduction [section, in DoubleInduction]
NBaseProp.DoubleInduction.R [variable, in R]
NBaseProp.DoubleInduction.R_wd [variable, in R_wd]
NBaseProp.double_induction [lemma, in double_induction]
NBaseProp.eq_pred_0 [lemma, in eq_pred_0]
NBaseProp.induction [lemma, in induction]
NBaseProp.le_0_l [lemma, in le_0_l]
NBaseProp.neq_0_r [lemma, in neq_0_r]
NBaseProp.neq_0 [lemma, in neq_0]
NBaseProp.neq_succ_0 [lemma, in neq_succ_0]
NBaseProp.neq_0_succ [lemma, in neq_0_succ]
NBaseProp.PairInduction [section, in PairInduction]
NBaseProp.PairInduction.A [variable, in A]
NBaseProp.PairInduction.A_wd [variable, in A_wd]
NBaseProp.pair_induction [lemma, in pair_induction]
NBaseProp.pred_inj [lemma, in pred_inj]
NBaseProp.succ_pred [lemma, in succ_pred]
NBaseProp.TwoDimensionalInduction [section, in TwoDimensionalInduction]
NBaseProp.TwoDimensionalInduction.R [variable, in R]
NBaseProp.TwoDimensionalInduction.R_wd [variable, in R_wd]
NBaseProp.two_dim_induction [lemma, in two_dim_induction]
NBaseProp.zero_or_succ [lemma, in zero_or_succ]
Nbasic [library]
NBinary [library]
Nbit [abbreviation, in Nbit]
NBits [library]
NBitsProp [module, in NBitsProp]
NBitsProp.add_bit0 [lemma, in add_bit0]
NBitsProp.add_bit1 [lemma, in add_bit1]
NBitsProp.add_b2n_double_div2 [lemma, in add_b2n_double_div2]
NBitsProp.add_nocarry_mod_lt_pow2 [lemma, in add_nocarry_mod_lt_pow2]
NBitsProp.add_carry_div2 [lemma, in add_carry_div2]
NBitsProp.add_lnot_diag_low [lemma, in add_lnot_diag_low]
NBitsProp.add_nocarry_lxor [lemma, in add_nocarry_lxor]
NBitsProp.add_nocarry_lt_pow2 [lemma, in add_nocarry_lt_pow2]
NBitsProp.add_carry_bits [lemma, in add_carry_bits]
NBitsProp.add_b2n_double_bit0 [lemma, in add_b2n_double_bit0]
NBitsProp.add3_bits_div2 [lemma, in add3_bits_div2]
NBitsProp.add3_bit0 [lemma, in add3_bit0]
NBitsProp.are_bits [lemma, in are_bits]
NBitsProp.bits_above_log2 [lemma, in bits_above_log2]
NBitsProp.bits_0 [lemma, in bits_0]
NBitsProp.bits_inj_0 [lemma, in bits_inj_0]
NBitsProp.bits_inj_iff [lemma, in bits_inj_iff]
NBitsProp.bits_inj [lemma, in bits_inj]
NBitsProp.bit_log2 [lemma, in bit_log2]
NBitsProp.bit0_eqb [lemma, in bit0_eqb]
NBitsProp.bit0_odd [lemma, in bit0_odd]
NBitsProp.bit0_mod [lemma, in bit0_mod]
NBitsProp.b2n [definition, in b2n]
NBitsProp.b2n_bit0 [lemma, in b2n_bit0]
NBitsProp.b2n_proper [instance, in b2n_proper]
NBitsProp.b2n_inj [lemma, in b2n_inj]
NBitsProp.b2n_div2 [lemma, in b2n_div2]
NBitsProp.clearbit [definition, in clearbit]
NBitsProp.clearbit_spec' [lemma, in clearbit_spec']
NBitsProp.clearbit_iff [lemma, in clearbit_iff]
NBitsProp.clearbit_eq [lemma, in clearbit_eq]
NBitsProp.clearbit_neq [lemma, in clearbit_neq]
NBitsProp.clearbit_eqb [lemma, in clearbit_eqb]
NBitsProp.clearbit_wd [instance, in clearbit_wd]
NBitsProp.div_pow2_bits [lemma, in div_pow2_bits]
NBitsProp.div2_wd [instance, in div2_wd]
NBitsProp.div2_div [lemma, in div2_div]
NBitsProp.div2_bits [lemma, in div2_bits]
NBitsProp.div2_odd [lemma, in div2_odd]
NBitsProp.double_bits_succ [lemma, in double_bits_succ]
NBitsProp.eqf [definition, in eqf]
NBitsProp.eqf_equiv [instance, in eqf_equiv]
NBitsProp.exists_div2 [lemma, in exists_div2]
NBitsProp.land_comm [lemma, in land_comm]
NBitsProp.land_assoc [lemma, in land_assoc]
NBitsProp.land_0_l [lemma, in land_0_l]
NBitsProp.land_wd [instance, in land_wd]
NBitsProp.land_ones_low [lemma, in land_ones_low]
NBitsProp.land_ldiff [lemma, in land_ldiff]
NBitsProp.land_lnot_diag [lemma, in land_lnot_diag]
NBitsProp.land_lor_distr_r [lemma, in land_lor_distr_r]
NBitsProp.land_ones [lemma, in land_ones]
NBitsProp.land_diag [lemma, in land_diag]
NBitsProp.land_lnot_diag_low [lemma, in land_lnot_diag_low]
NBitsProp.land_0_r [lemma, in land_0_r]
NBitsProp.land_lor_distr_l [lemma, in land_lor_distr_l]
NBitsProp.ldiff_wd [instance, in ldiff_wd]
NBitsProp.ldiff_land_low [lemma, in ldiff_land_low]
NBitsProp.ldiff_ldiff_l [lemma, in ldiff_ldiff_l]
NBitsProp.ldiff_ones_r_low [lemma, in ldiff_ones_r_low]
NBitsProp.ldiff_ones_r [lemma, in ldiff_ones_r]
NBitsProp.ldiff_ones_l_low [lemma, in ldiff_ones_l_low]
NBitsProp.ldiff_diag [lemma, in ldiff_diag]
NBitsProp.ldiff_le [lemma, in ldiff_le]
NBitsProp.ldiff_0_l [lemma, in ldiff_0_l]
NBitsProp.ldiff_0_r [lemma, in ldiff_0_r]
NBitsProp.lnextcarry [abbreviation, in lnextcarry]
NBitsProp.lnot [definition, in lnot]
NBitsProp.lnot_ldiff_low [lemma, in lnot_ldiff_low]
NBitsProp.lnot_lor_low [lemma, in lnot_lor_low]
NBitsProp.lnot_land_low [lemma, in lnot_land_low]
NBitsProp.lnot_spec_high [lemma, in lnot_spec_high]
NBitsProp.lnot_wd [instance, in lnot_wd]
NBitsProp.lnot_lxor_l [lemma, in lnot_lxor_l]
NBitsProp.lnot_ones [lemma, in lnot_ones]
NBitsProp.lnot_0_l [lemma, in lnot_0_l]
NBitsProp.lnot_lxor_r [lemma, in lnot_lxor_r]
NBitsProp.lnot_involutive [lemma, in lnot_involutive]
NBitsProp.lnot_sub_low [lemma, in lnot_sub_low]
NBitsProp.lnot_spec_low [lemma, in lnot_spec_low]
NBitsProp.log2_lor [lemma, in log2_lor]
NBitsProp.log2_shiftr [lemma, in log2_shiftr]
NBitsProp.log2_lxor [lemma, in log2_lxor]
NBitsProp.log2_bits_unique [lemma, in log2_bits_unique]
NBitsProp.log2_shiftl [lemma, in log2_shiftl]
NBitsProp.log2_land [lemma, in log2_land]
NBitsProp.lor_comm [lemma, in lor_comm]
NBitsProp.lor_eq_0_iff [lemma, in lor_eq_0_iff]
NBitsProp.lor_ldiff_and [lemma, in lor_ldiff_and]
NBitsProp.lor_land_distr_r [lemma, in lor_land_distr_r]
NBitsProp.lor_eq_0_l [lemma, in lor_eq_0_l]
NBitsProp.lor_land_distr_l [lemma, in lor_land_distr_l]
NBitsProp.lor_lnot_diag [lemma, in lor_lnot_diag]
NBitsProp.lor_wd [instance, in lor_wd]
NBitsProp.lor_0_r [lemma, in lor_0_r]
NBitsProp.lor_ones_low [lemma, in lor_ones_low]
NBitsProp.lor_assoc [lemma, in lor_assoc]
NBitsProp.lor_diag [lemma, in lor_diag]
NBitsProp.lor_0_l [lemma, in lor_0_l]
NBitsProp.lor_lnot_diag_low [lemma, in lor_lnot_diag_low]
NBitsProp.lxor_wd [instance, in lxor_wd]
NBitsProp.lxor_lnot_lnot [lemma, in lxor_lnot_lnot]
NBitsProp.lxor_0_r [lemma, in lxor_0_r]
NBitsProp.lxor_0_l [lemma, in lxor_0_l]
NBitsProp.lxor_lor [lemma, in lxor_lor]
NBitsProp.lxor_eq_0_iff [lemma, in lxor_eq_0_iff]
NBitsProp.lxor_comm [lemma, in lxor_comm]
NBitsProp.lxor_assoc [lemma, in lxor_assoc]
NBitsProp.lxor_eq [lemma, in lxor_eq]
NBitsProp.lxor_nilpotent [lemma, in lxor_nilpotent]
NBitsProp.lxor3 [abbreviation, in lxor3]
NBitsProp.mod_pow2_bits_high [lemma, in mod_pow2_bits_high]
NBitsProp.mod_pow2_bits_low [lemma, in mod_pow2_bits_low]
NBitsProp.mul_pow2_bits_high [lemma, in mul_pow2_bits_high]
NBitsProp.mul_pow2_bits_low [lemma, in mul_pow2_bits_low]
NBitsProp.mul_pow2_bits_add [lemma, in mul_pow2_bits_add]
NBitsProp.nextcarry [abbreviation, in nextcarry]
NBitsProp.nocarry_equiv [lemma, in nocarry_equiv]
NBitsProp.ones [definition, in ones]
NBitsProp.ones_mod_pow2 [lemma, in ones_mod_pow2]
NBitsProp.ones_div_pow2 [lemma, in ones_div_pow2]
NBitsProp.ones_spec_iff [lemma, in ones_spec_iff]
NBitsProp.ones_wd [instance, in ones_wd]
NBitsProp.ones_add [lemma, in ones_add]
NBitsProp.ones_equiv [lemma, in ones_equiv]
NBitsProp.ones_spec_low [lemma, in ones_spec_low]
NBitsProp.ones_spec_high [lemma, in ones_spec_high]
NBitsProp.pow_div_l [lemma, in pow_div_l]
NBitsProp.pow_sub_r [lemma, in pow_sub_r]
NBitsProp.pow2_bits_eqb [lemma, in pow2_bits_eqb]
NBitsProp.pow2_bits_false [lemma, in pow2_bits_false]
NBitsProp.pow2_bits_true [lemma, in pow2_bits_true]
NBitsProp.setbit [definition, in setbit]
NBitsProp.setbit_neq [lemma, in setbit_neq]
NBitsProp.setbit_eqb [lemma, in setbit_eqb]
NBitsProp.setbit_eq [lemma, in setbit_eq]
NBitsProp.setbit_spec' [lemma, in setbit_spec']
NBitsProp.setbit_wd [instance, in setbit_wd]
NBitsProp.setbit_iff [lemma, in setbit_iff]
NBitsProp.shiftl_land [lemma, in shiftl_land]
NBitsProp.shiftl_lxor [lemma, in shiftl_lxor]
NBitsProp.shiftl_1_l [lemma, in shiftl_1_l]
NBitsProp.shiftl_wd [instance, in shiftl_wd]
NBitsProp.shiftl_eq_0_iff [lemma, in shiftl_eq_0_iff]
NBitsProp.shiftl_0_l [lemma, in shiftl_0_l]
NBitsProp.shiftl_mul_pow2 [lemma, in shiftl_mul_pow2]
NBitsProp.shiftl_ldiff [lemma, in shiftl_ldiff]
NBitsProp.shiftl_0_r [lemma, in shiftl_0_r]
NBitsProp.shiftl_shiftl [lemma, in shiftl_shiftl]
NBitsProp.shiftl_spec_alt [lemma, in shiftl_spec_alt]
NBitsProp.shiftl_spec_high' [lemma, in shiftl_spec_high']
NBitsProp.shiftl_lor [lemma, in shiftl_lor]
NBitsProp.shiftr_div_pow2 [lemma, in shiftr_div_pow2]
NBitsProp.shiftr_ldiff [lemma, in shiftr_ldiff]
NBitsProp.shiftr_lxor [lemma, in shiftr_lxor]
NBitsProp.shiftr_0_l [lemma, in shiftr_0_l]
NBitsProp.shiftr_spec' [lemma, in shiftr_spec']
NBitsProp.shiftr_shiftl_l [lemma, in shiftr_shiftl_l]
NBitsProp.shiftr_wd [instance, in shiftr_wd]
NBitsProp.shiftr_eq_0 [lemma, in shiftr_eq_0]
NBitsProp.shiftr_shiftl_r [lemma, in shiftr_shiftl_r]
NBitsProp.shiftr_land [lemma, in shiftr_land]
NBitsProp.shiftr_lor [lemma, in shiftr_lor]
NBitsProp.shiftr_0_r [lemma, in shiftr_0_r]
NBitsProp.shiftr_shiftr [lemma, in shiftr_shiftr]
NBitsProp.shiftr_eq_0_iff [lemma, in shiftr_eq_0_iff]
NBitsProp.sub_nocarry_ldiff [lemma, in sub_nocarry_ldiff]
NBitsProp.testbit_0_r [lemma, in testbit_0_r]
NBitsProp.testbit_true [lemma, in testbit_true]
NBitsProp.testbit_eqb [lemma, in testbit_eqb]
NBitsProp.testbit_false [lemma, in testbit_false]
NBitsProp.testbit_unique [lemma, in testbit_unique]
NBitsProp.testbit_spec [lemma, in testbit_spec]
NBitsProp.testbit_eqf [instance, in testbit_eqf]
NBitsProp.testbit_spec' [lemma, in testbit_spec']
NBitsProp.testbit_succ_r [lemma, in testbit_succ_r]
NBitsProp.testbit_odd [lemma, in testbit_odd]
NBitsProp.xor3 [abbreviation, in xor3]
_ === _ [notation, in ::x_'==='_x]
Nbit_faithful [lemma, in Nbit_faithful]
Nbit_faithful_iff [lemma, in Nbit_faithful_iff]
Nbit_Ntestbit [lemma, in Nbit_Ntestbit]
Nbit_Nsize [lemma, in Nbit_Nsize]
Nbit_Bth [lemma, in Nbit_Bth]
Nbit0 [abbreviation, in Nbit0]
Nbit0_less [lemma, in Nbit0_less]
Nbit0_neq [lemma, in Nbit0_neq]
Nbit0_correct [lemma, in Nbit0_correct]
Nbit0_gt [lemma, in Nbit0_gt]
Nbit0_Blow [lemma, in Nbit0_Blow]
Nbound [definition, in Nbound]
Ncompare [abbreviation, in Ncompare]
Ncompare_refl [abbreviation, in Ncompare_refl]
Ncompare_Lt_Nltb [lemma, in Ncompare_Lt_Nltb]
Ncompare_Gt_Nltb [lemma, in Ncompare_Gt_Nltb]
Ncompare_eq_correct [abbreviation, in Ncompare_eq_correct]
Ncompare_spec [abbreviation, in Ncompare_spec]
Ncompare_antisym [lemma, in Ncompare_antisym]
Ncompare_Neqb [lemma, in Ncompare_Neqb]
Ncompare_0 [abbreviation, in Ncompare_0]
Ncompare_Eq_eq [abbreviation, in Ncompare_Eq_eq]
ncurry [definition, in ncurry]
Ndec [library]
NDefOps [library]
NdefOpsProp [module, in NdefOpsProp]
NdefOpsProp.def_add_wd [instance, in def_add_wd]
NdefOpsProp.def_mul_wd [instance, in def_mul_wd]
NdefOpsProp.def_add [definition, in def_add]
NdefOpsProp.def_add_0_l [lemma, in def_add_0_l]
NdefOpsProp.def_add_add [lemma, in def_add_add]
NdefOpsProp.def_add_succ_l [lemma, in def_add_succ_l]
NdefOpsProp.def_mul [definition, in def_mul]
NdefOpsProp.def_mul_0_r [lemma, in def_mul_0_r]
NdefOpsProp.def_mul_succ_r [lemma, in def_mul_succ_r]
NdefOpsProp.def_mul_mul [lemma, in def_mul_mul]
NdefOpsProp.even [definition, in even]
NdefOpsProp.even_0 [lemma, in even_0]
NdefOpsProp.even_wd [instance, in even_wd]
NdefOpsProp.even_succ [lemma, in even_succ]
NdefOpsProp.half [definition, in half]
NdefOpsProp.half_aux_0 [lemma, in half_aux_0]
NdefOpsProp.half_aux_succ [lemma, in half_aux_succ]
NdefOpsProp.half_aux_spec2 [lemma, in half_aux_spec2]
NdefOpsProp.half_upper_bound [lemma, in half_upper_bound]
NdefOpsProp.half_aux_spec [lemma, in half_aux_spec]
NdefOpsProp.half_0 [lemma, in half_0]
NdefOpsProp.half_aux_wd [instance, in half_aux_wd]
NdefOpsProp.half_1 [lemma, in half_1]
NdefOpsProp.half_nz [lemma, in half_nz]
NdefOpsProp.half_lower_bound [lemma, in half_lower_bound]
NdefOpsProp.half_wd [instance, in half_wd]
NdefOpsProp.half_double [lemma, in half_double]
NdefOpsProp.half_decrease [lemma, in half_decrease]
NdefOpsProp.half_aux [definition, in half_aux]
NdefOpsProp.if_zero_wd [instance, in if_zero_wd]
NdefOpsProp.if_zero_0 [lemma, in if_zero_0]
NdefOpsProp.if_zero [definition, in if_zero]
NdefOpsProp.if_zero_succ [lemma, in if_zero_succ]
NdefOpsProp.log [definition, in log]
NdefOpsProp.log_init [lemma, in log_init]
NdefOpsProp.log_step [lemma, in log_step]
NdefOpsProp.log_prewd [instance, in log_prewd]
NdefOpsProp.log_good_step [lemma, in log_good_step]
NdefOpsProp.log_wd [instance, in log_wd]
NdefOpsProp.ltb [definition, in ltb]
NdefOpsProp.ltb_step [lemma, in ltb_step]
NdefOpsProp.ltb_ge [lemma, in ltb_ge]
NdefOpsProp.ltb_0 [lemma, in ltb_0]
NdefOpsProp.ltb_wd [instance, in ltb_wd]
NdefOpsProp.ltb_0_succ [lemma, in ltb_0_succ]
NdefOpsProp.ltb_base [lemma, in ltb_base]
NdefOpsProp.ltb_lt [lemma, in ltb_lt]
NdefOpsProp.pow [definition, in pow]
NdefOpsProp.pow_wd [instance, in pow_wd]
NdefOpsProp.pow_succ [lemma, in pow_succ]
NdefOpsProp.pow_0 [lemma, in pow_0]
NdefOpsProp.pow2_log [lemma, in pow2_log]
NdefOpsProp.succ_ltb_mono [lemma, in succ_ltb_mono]
_ ** _ [notation, in ::x_'**'_x]
_ ^^ _ [notation, in ::x_'^^'_x]
_ +++ _ [notation, in ::x_'+++'_x]
_ << _ [notation, in ::x_'<<'_x]
Ndiff_semantics [lemma, in Ndiff_semantics]
Ndigits [library]
Ndiscr [abbreviation, in Ndiscr]
Ndist [library]
Ndiv [abbreviation, in Ndiv]
NDiv [library]
Ndivide [abbreviation, in Ndivide]
NDivProp [module, in NDivProp]
NDivProp.add_mod_idemp_r [lemma, in add_mod_idemp_r]
NDivProp.add_mod_idemp_l [lemma, in add_mod_idemp_l]
NDivProp.add_mod [lemma, in add_mod]
NDivProp.div_mod_unique [lemma, in div_mod_unique]
NDivProp.div_unique [lemma, in div_unique]
NDivProp.div_small_iff [lemma, in div_small_iff]
NDivProp.div_mul_le [lemma, in div_mul_le]
NDivProp.div_mul [lemma, in div_mul]
NDivProp.div_0_l [lemma, in div_0_l]
NDivProp.div_div [lemma, in div_div]
NDivProp.div_add [lemma, in div_add]
NDivProp.div_1_l [lemma, in div_1_l]
NDivProp.div_exact [lemma, in div_exact]
NDivProp.div_le_mono [lemma, in div_le_mono]
NDivProp.div_same [lemma, in div_same]
NDivProp.div_unique_exact [lemma, in div_unique_exact]
NDivProp.div_mul_cancel_r [lemma, in div_mul_cancel_r]
NDivProp.div_le_compat_l [lemma, in div_le_compat_l]
NDivProp.div_le_upper_bound [lemma, in div_le_upper_bound]
NDivProp.div_lt [lemma, in div_lt]
NDivProp.div_mul_cancel_l [lemma, in div_mul_cancel_l]
NDivProp.div_le_lower_bound [lemma, in div_le_lower_bound]
NDivProp.div_small [lemma, in div_small]
NDivProp.div_str_pos_iff [lemma, in div_str_pos_iff]
NDivProp.div_str_pos [lemma, in div_str_pos]
NDivProp.div_1_r [lemma, in div_1_r]
NDivProp.div_lt_upper_bound [lemma, in div_lt_upper_bound]
NDivProp.div_add_l [lemma, in div_add_l]
NDivProp.mod_1_r [lemma, in mod_1_r]
NDivProp.mod_small_iff [lemma, in mod_small_iff]
NDivProp.mod_mul_r [lemma, in mod_mul_r]
NDivProp.mod_unique [lemma, in mod_unique]
NDivProp.mod_upper_bound [lemma, in mod_upper_bound]
NDivProp.mod_le [lemma, in mod_le]
NDivProp.mod_add [lemma, in mod_add]
NDivProp.mod_small [lemma, in mod_small]
NDivProp.mod_mod [lemma, in mod_mod]
NDivProp.mod_divides [lemma, in mod_divides]
NDivProp.mod_eq [lemma, in mod_eq]
NDivProp.mod_0_l [lemma, in mod_0_l]
NDivProp.mod_mul [lemma, in mod_mul]
NDivProp.mod_same [lemma, in mod_same]
NDivProp.mod_1_l [lemma, in mod_1_l]
NDivProp.mul_succ_div_gt [lemma, in mul_succ_div_gt]
NDivProp.mul_mod [lemma, in mul_mod]
NDivProp.mul_mod_distr_r [lemma, in mul_mod_distr_r]
NDivProp.mul_mod_distr_l [lemma, in mul_mod_distr_l]
NDivProp.mul_mod_idemp_r [lemma, in mul_mod_idemp_r]
NDivProp.mul_mod_idemp_l [lemma, in mul_mod_idemp_l]
NDivProp.mul_div_le [lemma, in mul_div_le]
NDivProp.Private_NZDiv [module, in NDivProp.Private_NZDiv]
NDivSpecific [module, in NDivSpecific]
NDivSpecific.mod_upper_bound [axiom, in mod_upper_bound]
Ndiv_Zquot [abbreviation, in Ndiv_Zquot]
Ndiv_mod_eq [abbreviation, in Ndiv_mod_eq]
Ndiv_eucl [abbreviation, in Ndiv_eucl]
Ndiv_eucl_correct [abbreviation, in Ndiv_eucl_correct]
Ndiv_def [library]
Ndiv2 [abbreviation, in Ndiv2]
Ndiv2_double_plus_one [lemma, in Ndiv2_double_plus_one]
Ndiv2_bit_eq [lemma, in Ndiv2_bit_eq]
Ndiv2_correct [lemma, in Ndiv2_correct]
Ndiv2_double [lemma, in Ndiv2_double]
Ndiv2_eq [lemma, in Ndiv2_eq]
Ndiv2_bit_neq [lemma, in Ndiv2_bit_neq]
Ndiv2_neq [lemma, in Ndiv2_neq]
Ndouble [abbreviation, in Ndouble]
Ndouble_plus_one_div2 [abbreviation, in Ndouble_plus_one_div2]
Ndouble_inj [abbreviation, in Ndouble_inj]
Ndouble_div2 [abbreviation, in Ndouble_div2]
Ndouble_plus_one [abbreviation, in Ndouble_plus_one]
Ndouble_bit0 [lemma, in Ndouble_bit0]
Ndouble_plus_one_inj [abbreviation, in Ndouble_plus_one_inj]
Ndouble_plus_one_bit0 [lemma, in Ndouble_plus_one_bit0]
Ndouble_or_double_plus_un [lemma, in Ndouble_or_double_plus_un]
neg [projection, in neg]
negative_derivative [lemma, in negative_derivative]
negb [definition, in negb]
negb_true_iff [lemma, in negb_true_iff]
negb_orb [lemma, in negb_orb]
negb_prop_elim [lemma, in negb_prop_elim]
negb_sym [lemma, in negb_sym]
negb_prop_involutive [lemma, in negb_prop_involutive]
negb_andb [lemma, in negb_andb]
negb_false_iff [lemma, in negb_false_iff]
negb_intro [abbreviation, in negb_intro]
negb_prop_intro [lemma, in negb_prop_intro]
negb_elim [abbreviation, in negb_elim]
negb_involutive [lemma, in negb_involutive]
negb_if [lemma, in negb_if]
negb_involutive_reverse [lemma, in negb_involutive_reverse]
negb_prop_classical [lemma, in negb_prop_classical]
negb_xorb_r [lemma, in negb_xorb_r]
negb_xorb_l [lemma, in negb_xorb_l]
negreal [record, in negreal]
neg_cos [lemma, in neg_cos]
neg_sin [lemma, in neg_sin]
neg_false [lemma, in neg_false]
neg_pos_Rsqr_le [lemma, in neg_pos_Rsqr_le]
neighbourhood [definition, in neighbourhood]
neighbourhood_P1 [lemma, in neighbourhood_P1]
neq [definition, in neq]
Neqb [abbreviation, in Neqb]
Neqb [abbreviation, in Neqb]
Neqb_eq [abbreviation, in Neqb_eq]
Neqb_comm [abbreviation, in Neqb_comm]
Neqb_complete [lemma, in Neqb_complete]
Neqb_correct [abbreviation, in Neqb_correct]
Neqb_Ncompare [lemma, in Neqb_Ncompare]
nequiv_decb [definition, in nequiv_decb]
nequiv_decb [definition, in nequiv_decb]
nequiv_equiv_trans [lemma, in nequiv_equiv_trans]
nequiv_dec [definition, in nequiv_dec]
nequiv_dec [definition, in nequiv_dec]
neq_0_lt [lemma, in neq_0_lt]
neq_O_lt [abbreviation, in neq_O_lt]
Neven [definition, in Neven]
Neven [abbreviation, in Neven]
Neven_not_double_plus_one [lemma, in Neven_not_double_plus_one]
Neven_spec [abbreviation, in Neven_spec]
Newman [lemma, in Newman]
NewtonInt [definition, in NewtonInt]
NewtonInt [library]
NewtonInt_P4 [lemma, in NewtonInt_P4]
NewtonInt_P6 [lemma, in NewtonInt_P6]
NewtonInt_P7 [lemma, in NewtonInt_P7]
NewtonInt_P5 [lemma, in NewtonInt_P5]
NewtonInt_P1 [lemma, in NewtonInt_P1]
NewtonInt_P9 [lemma, in NewtonInt_P9]
NewtonInt_P2 [lemma, in NewtonInt_P2]
NewtonInt_P3 [lemma, in NewtonInt_P3]
NewtonInt_P8 [lemma, in NewtonInt_P8]
Newton_integrable [definition, in Newton_integrable]
next [constructor, in next]
nfold [definition, in nfold]
nfold_list [definition, in nfold_list]
nfold_bis [definition, in nfold_bis]
nfun [definition, in nfun]
nfun_to_nfun [definition, in nfun_to_nfun]
nfun_to_nfun_bis [definition, in nfun_to_nfun_bis]
Ngcd [abbreviation, in Ngcd]
NGcd [library]
NGcdProp [module, in NGcdProp]
NGcdProp.Bezout [definition, in Bezout]
NGcdProp.Bezout_wd [instance, in Bezout_wd]
NGcdProp.bezout_1_gcd [lemma, in bezout_1_gcd]
NGcdProp.divide_1_r [definition, in divide_1_r]
NGcdProp.divide_antisym [definition, in divide_antisym]
NGcdProp.divide_mul_split [lemma, in divide_mul_split]
NGcdProp.divide_add_cancel_r [lemma, in divide_add_cancel_r]
NGcdProp.divide_gcd_iff' [definition, in divide_gcd_iff']
NGcdProp.divide_sub_r [lemma, in divide_sub_r]
NGcdProp.gauss [lemma, in gauss]
NGcdProp.gcd_mul_mono_l [lemma, in gcd_mul_mono_l]
NGcdProp.gcd_add_mult_diag_r [lemma, in gcd_add_mult_diag_r]
NGcdProp.gcd_unique_alt' [definition, in gcd_unique_alt']
NGcdProp.gcd_bezout_pos [lemma, in gcd_bezout_pos]
NGcdProp.gcd_0_r [definition, in gcd_0_r]
NGcdProp.gcd_mul_mono_r [lemma, in gcd_mul_mono_r]
NGcdProp.gcd_0_l [definition, in gcd_0_l]
NGcdProp.gcd_diag [definition, in gcd_diag]
NGcdProp.gcd_sub_diag_r [lemma, in gcd_sub_diag_r]
NGcdProp.gcd_bezout_pos_pos [lemma, in gcd_bezout_pos_pos]
NGcdProp.gcd_add_diag_r [lemma, in gcd_add_diag_r]
NGcdProp.gcd_unique' [definition, in gcd_unique']
NGcdProp.gcd_bezout [lemma, in gcd_bezout]
Ngcd_divide_r [abbreviation, in Ngcd_divide_r]
Ngcd_greatest [abbreviation, in Ngcd_greatest]
Ngcd_divide_l [abbreviation, in Ngcd_divide_l]
Ngcd_def [library]
Nge [abbreviation, in Nge]
Nggcd [abbreviation, in Nggcd]
Nggcd_correct_divisors [abbreviation, in Nggcd_correct_divisors]
Nggcd_gcd [abbreviation, in Nggcd_gcd]
Ngt [abbreviation, in Ngt]
Ngt_Nlt [abbreviation, in Ngt_Nlt]
ni [constructor, in ni]
Nil [abbreviation, in Nil]
nil [constructor, in nil]
nil [constructor, in nil]
nil [abbreviation, in nil]
nil [constructor, in nil]
nil_is_heap [constructor, in nil_is_heap]
nil_sort [abbreviation, in nil_sort]
nil_leA [abbreviation, in nil_leA]
nil_cons [lemma, in nil_cons]
Nind [abbreviation, in Nind]
NIso [library]
ni_le_min_2 [lemma, in ni_le_min_2]
ni_le_min_1 [lemma, in ni_le_min_1]
ni_min_idemp [lemma, in ni_min_idemp]
ni_le [definition, in ni_le]
ni_le_antisym [lemma, in ni_le_antisym]
ni_le_trans [lemma, in ni_le_trans]
ni_min_inf_l [lemma, in ni_min_inf_l]
ni_min_comm [lemma, in ni_min_comm]
ni_min_case [lemma, in ni_min_case]
ni_min_assoc [lemma, in ni_min_assoc]
ni_le_min_induc [lemma, in ni_le_min_induc]
ni_le_total [lemma, in ni_le_total]
ni_le_le [lemma, in ni_le_le]
ni_min [definition, in ni_min]
ni_min_O_r [lemma, in ni_min_O_r]
ni_le_refl [lemma, in ni_le_refl]
ni_min_O_l [lemma, in ni_min_O_l]
ni_min_inf_r [lemma, in ni_min_inf_r]
NLcm [library]
NLcmProp [module, in NLcmProp]
NLcmProp.divide_lcm_l [lemma, in divide_lcm_l]
NLcmProp.divide_lcm_iff [lemma, in divide_lcm_iff]
NLcmProp.divide_lcm_r [lemma, in divide_lcm_r]
NLcmProp.divide_div [lemma, in divide_div]
NLcmProp.divide_lcm_eq_r [lemma, in divide_lcm_eq_r]
NLcmProp.divide_div_mul_exact [lemma, in divide_div_mul_exact]
NLcmProp.gcd_1_lcm_mul [lemma, in gcd_1_lcm_mul]
NLcmProp.gcd_div_factor [lemma, in gcd_div_factor]
NLcmProp.gcd_div_gcd [lemma, in gcd_div_gcd]
NLcmProp.gcd_div_swap [lemma, in gcd_div_swap]
NLcmProp.gcd_mod [lemma, in gcd_mod]
NLcmProp.lcm [definition, in lcm]
NLcmProp.lcm_1_l [lemma, in lcm_1_l]
NLcmProp.lcm_0_l [lemma, in lcm_0_l]
NLcmProp.lcm_0_r [lemma, in lcm_0_r]
NLcmProp.lcm_least [lemma, in lcm_least]
NLcmProp.lcm_wd [instance, in lcm_wd]
NLcmProp.lcm_equiv1 [lemma, in lcm_equiv1]
NLcmProp.lcm_1_r [lemma, in lcm_1_r]
NLcmProp.lcm_mul_mono_l [lemma, in lcm_mul_mono_l]
NLcmProp.lcm_unique_alt [lemma, in lcm_unique_alt]
NLcmProp.lcm_eq_0 [lemma, in lcm_eq_0]
NLcmProp.lcm_unique [lemma, in lcm_unique]
NLcmProp.lcm_divide_iff [lemma, in lcm_divide_iff]
NLcmProp.lcm_assoc [lemma, in lcm_assoc]
NLcmProp.lcm_equiv2 [lemma, in lcm_equiv2]
NLcmProp.lcm_comm [lemma, in lcm_comm]
NLcmProp.lcm_mul_mono_r [lemma, in lcm_mul_mono_r]
NLcmProp.lcm_diag [lemma, in lcm_diag]
NLcmProp.mod_divide [lemma, in mod_divide]
Nle [abbreviation, in Nle]
Nleb [definition, in Nleb]
Nleb_double_mono_conv [lemma, in Nleb_double_mono_conv]
Nleb_double_plus_one_mono_conv [lemma, in Nleb_double_plus_one_mono_conv]
Nleb_alt [lemma, in Nleb_alt]
Nleb_Nle [lemma, in Nleb_Nle]
Nleb_refl [lemma, in Nleb_refl]
Nleb_antisym [lemma, in Nleb_antisym]
Nleb_double_mono [lemma, in Nleb_double_mono]
Nleb_trans [lemma, in Nleb_trans]
Nleb_ltb_trans [lemma, in Nleb_ltb_trans]
Nleb_double_plus_one_mono [lemma, in Nleb_double_plus_one_mono]
Nless [definition, in Nless]
Nless_not_refl [lemma, in Nless_not_refl]
Nless_z [lemma, in Nless_z]
Nless_def_3 [lemma, in Nless_def_3]
Nless_def_2 [lemma, in Nless_def_2]
Nless_def_4 [lemma, in Nless_def_4]
Nless_def_1 [lemma, in Nless_def_1]
Nless_total [lemma, in Nless_total]
Nless_aux [definition, in Nless_aux]
Nless_trans [lemma, in Nless_trans]
Nle_succ_l [abbreviation, in Nle_succ_l]
Nle_trans [abbreviation, in Nle_trans]
Nle_0 [abbreviation, in Nle_0]
Nle_lteq [abbreviation, in Nle_lteq]
NLog [library]
Nlog2 [abbreviation, in Nlog2]
NLog2Prop [module, in NLog2Prop]
Nlog2_spec [abbreviation, in Nlog2_spec]
Nlog2_nonpos [abbreviation, in Nlog2_nonpos]
Nlt [abbreviation, in Nlt]
Nltb_double_mono_conv [lemma, in Nltb_double_mono_conv]
Nltb_double_mono [lemma, in Nltb_double_mono]
Nltb_trans [lemma, in Nltb_trans]
Nltb_double_plus_one_mono_conv [lemma, in Nltb_double_plus_one_mono_conv]
Nltb_leb_weak [lemma, in Nltb_leb_weak]
Nltb_double_plus_one_mono [lemma, in Nltb_double_plus_one_mono]
Nltb_leb_trans [lemma, in Nltb_leb_trans]
Nltb_Ncompare [lemma, in Nltb_Ncompare]
Nlt_irrefl [abbreviation, in Nlt_irrefl]
Nlt_not_eq [abbreviation, in Nlt_not_eq]
Nlt_trans [abbreviation, in Nlt_trans]
Nlt_succ_r [abbreviation, in Nlt_succ_r]
NMake [library]
NMake_gen [library]
Nmax [abbreviation, in Nmax]
NMaxMin [library]
NMaxMinProp [module, in NMaxMinProp]
NMaxMinProp.add_max_distr_r [lemma, in add_max_distr_r]
NMaxMinProp.add_min_distr_r [lemma, in add_min_distr_r]
NMaxMinProp.add_min_distr_l [lemma, in add_min_distr_l]
NMaxMinProp.add_max_distr_l [lemma, in add_max_distr_l]
NMaxMinProp.max_0_l [lemma, in max_0_l]
NMaxMinProp.max_0_r [lemma, in max_0_r]
NMaxMinProp.min_0_l [lemma, in min_0_l]
NMaxMinProp.min_0_r [lemma, in min_0_r]
NMaxMinProp.mul_min_distr_r [lemma, in mul_min_distr_r]
NMaxMinProp.mul_max_distr_r [lemma, in mul_max_distr_r]
NMaxMinProp.mul_max_distr_l [lemma, in mul_max_distr_l]
NMaxMinProp.mul_min_distr_l [lemma, in mul_min_distr_l]
NMaxMinProp.sub_max_distr_r [lemma, in sub_max_distr_r]
NMaxMinProp.sub_max_distr_l [lemma, in sub_max_distr_l]
NMaxMinProp.sub_min_distr_l [lemma, in sub_min_distr_l]
NMaxMinProp.sub_min_distr_r [lemma, in sub_min_distr_r]
NMaxMinProp.succ_min_distr [lemma, in succ_min_distr]
NMaxMinProp.succ_max_distr [lemma, in succ_max_distr]
Nmin [abbreviation, in Nmin]
Nminus [abbreviation, in Nminus]
Nminus_N0_Nle [abbreviation, in Nminus_N0_Nle]
Nminus_succ_r [abbreviation, in Nminus_succ_r]
Nminus_0_r [abbreviation, in Nminus_0_r]
Nmin_le_1 [lemma, in Nmin_le_1]
Nmin_le_2 [lemma, in Nmin_le_2]
Nmin_le_3 [lemma, in Nmin_le_3]
Nmin_lt_4 [lemma, in Nmin_lt_4]
Nmin_le_4 [lemma, in Nmin_le_4]
Nmin_choice [abbreviation, in Nmin_choice]
Nmin_lt_3 [lemma, in Nmin_lt_3]
Nmin_le_5 [lemma, in Nmin_le_5]
Nmod [abbreviation, in Nmod]
Nmod_lt [abbreviation, in Nmod_lt]
Nmod_Zrem [abbreviation, in Nmod_Zrem]
NMulOrder [library]
NMulOrderProp [module, in NMulOrderProp]
NMulOrderProp.eq_mul_1 [lemma, in eq_mul_1]
NMulOrderProp.lt_0_mul' [lemma, in lt_0_mul']
NMulOrderProp.mul_le_mono [lemma, in mul_le_mono]
NMulOrderProp.mul_pos [abbreviation, in mul_pos]
NMulOrderProp.mul_lt_mono [lemma, in mul_lt_mono]
NMulOrderProp.mul_le_mono_r [lemma, in mul_le_mono_r]
NMulOrderProp.mul_le_mono_l [lemma, in mul_le_mono_l]
NMulOrderProp.mul_eq_1 [definition, in mul_eq_1]
NMulOrderProp.square_lt_mono [lemma, in square_lt_mono]
NMulOrderProp.square_le_mono [lemma, in square_le_mono]
Nmult [abbreviation, in Nmult]
Nmult_plus_distr_r [abbreviation, in Nmult_plus_distr_r]
Nmult_comm [abbreviation, in Nmult_comm]
Nmult_plus_distr_l [lemma, in Nmult_plus_distr_l]
Nmult_0_l [abbreviation, in Nmult_0_l]
Nmult_1_l [abbreviation, in Nmult_1_l]
Nmult_assoc [abbreviation, in Nmult_assoc]
Nmult_1_r [abbreviation, in Nmult_1_r]
Nmult_reg_r [lemma, in Nmult_reg_r]
Nmult_Sn_m [lemma, in Nmult_Sn_m]
Nnat [library]
Nneg_bit0_2 [lemma, in Nneg_bit0_2]
Nneg_bit0_1 [lemma, in Nneg_bit0_1]
Nneg_bit0 [lemma, in Nneg_bit0]
Nneq_elim [lemma, in Nneq_elim]
Nnot_div2_not_double [lemma, in Nnot_div2_not_double]
Nnot_div2_not_double_plus_one [lemma, in Nnot_div2_not_double_plus_one]
NNPP [lemma, in NNPP]
Nodd [definition, in Nodd]
Nodd [abbreviation, in Nodd]
Nodd_not_double [lemma, in Nodd_not_double]
Nodd_spec [abbreviation, in Nodd_spec]
NodepOfDep [module, in NodepOfDep]
NodepOfDep.add [definition, in add]
NodepOfDep.Add [definition, in Add]
NodepOfDep.add_1 [lemma, in add_1]
NodepOfDep.add_2 [lemma, in add_2]
NodepOfDep.add_3 [lemma, in add_3]
NodepOfDep.cardinal [definition, in cardinal]
NodepOfDep.cardinal_1 [lemma, in cardinal_1]
NodepOfDep.choose [definition, in choose]
NodepOfDep.choose_3 [lemma, in choose_3]
NodepOfDep.choose_1 [lemma, in choose_1]
NodepOfDep.choose_2 [lemma, in choose_2]
NodepOfDep.compare [definition, in compare]
NodepOfDep.compat_P_aux [lemma, in compat_P_aux]
NodepOfDep.diff [definition, in diff]
NodepOfDep.diff_2 [lemma, in diff_2]
NodepOfDep.diff_1 [lemma, in diff_1]
NodepOfDep.diff_3 [lemma, in diff_3]
NodepOfDep.E [module, in NodepOfDep.E]
NodepOfDep.elements [definition, in elements]
NodepOfDep.elements_3w [lemma, in elements_3w]
NodepOfDep.elements_3 [lemma, in elements_3]
NodepOfDep.elements_1 [lemma, in elements_1]
NodepOfDep.elements_2 [lemma, in elements_2]
NodepOfDep.elt [definition, in elt]
NodepOfDep.empty [definition, in empty]
NodepOfDep.Empty [definition, in Empty]
NodepOfDep.empty_1 [lemma, in empty_1]
NodepOfDep.eq [definition, in eq]
NodepOfDep.equal [definition, in equal]
NodepOfDep.Equal [definition, in Equal]
NodepOfDep.equal_2 [lemma, in equal_2]
NodepOfDep.equal_1 [lemma, in equal_1]
NodepOfDep.eq_refl [definition, in eq_refl]
NodepOfDep.eq_sym [definition, in eq_sym]
NodepOfDep.eq_trans [definition, in eq_trans]
NodepOfDep.eq_dec [definition, in eq_dec]
NodepOfDep.Exists [definition, in Exists]
NodepOfDep.exists_1 [lemma, in exists_1]
NodepOfDep.exists_ [definition, in exists_]
NodepOfDep.exists_2 [lemma, in exists_2]
NodepOfDep.filter [definition, in filter]
NodepOfDep.filter_1 [lemma, in filter_1]
NodepOfDep.filter_3 [lemma, in filter_3]
NodepOfDep.filter_2 [lemma, in filter_2]
NodepOfDep.fold [definition, in fold]
NodepOfDep.fold_1 [lemma, in fold_1]
NodepOfDep.for_all_1 [lemma, in for_all_1]
NodepOfDep.for_all_2 [lemma, in for_all_2]
NodepOfDep.For_all [definition, in For_all]
NodepOfDep.for_all [definition, in for_all]
NodepOfDep.f_dec [definition, in f_dec]
NodepOfDep.In [definition, in In]
NodepOfDep.inter [definition, in inter]
NodepOfDep.inter_3 [lemma, in inter_3]
NodepOfDep.inter_2 [lemma, in inter_2]
NodepOfDep.inter_1 [lemma, in inter_1]
NodepOfDep.In_1 [definition, in In_1]
NodepOfDep.is_empty_1 [lemma, in is_empty_1]
NodepOfDep.is_empty [definition, in is_empty]
NodepOfDep.is_empty_2 [lemma, in is_empty_2]
NodepOfDep.lt [definition, in lt]
NodepOfDep.lt_not_eq [definition, in lt_not_eq]
NodepOfDep.lt_trans [definition, in lt_trans]
NodepOfDep.max_elt [definition, in max_elt]
NodepOfDep.max_elt_1 [lemma, in max_elt_1]
NodepOfDep.max_elt_3 [lemma, in max_elt_3]
NodepOfDep.max_elt_2 [lemma, in max_elt_2]
NodepOfDep.ME [module, in NodepOfDep.ME]
NodepOfDep.mem [definition, in mem]
NodepOfDep.mem_1 [lemma, in mem_1]
NodepOfDep.mem_2 [lemma, in mem_2]
NodepOfDep.min_elt_3 [lemma, in min_elt_3]
NodepOfDep.min_elt_2 [lemma, in min_elt_2]
NodepOfDep.min_elt_1 [lemma, in min_elt_1]
NodepOfDep.min_elt [definition, in min_elt]
NodepOfDep.partition [definition, in partition]
NodepOfDep.partition_1 [lemma, in partition_1]
NodepOfDep.partition_2 [lemma, in partition_2]
NodepOfDep.remove [definition, in remove]
NodepOfDep.remove_2 [lemma, in remove_2]
NodepOfDep.remove_1 [lemma, in remove_1]
NodepOfDep.remove_3 [lemma, in remove_3]
NodepOfDep.singleton [definition, in singleton]
NodepOfDep.singleton_1 [lemma, in singleton_1]
NodepOfDep.singleton_2 [lemma, in singleton_2]
NodepOfDep.Subset [definition, in Subset]
NodepOfDep.subset [definition, in subset]
NodepOfDep.subset_2 [lemma, in subset_2]
NodepOfDep.subset_1 [lemma, in subset_1]
NodepOfDep.t [definition, in t]
NodepOfDep.union [definition, in union]
NodepOfDep.union_1 [lemma, in union_1]
NodepOfDep.union_2 [lemma, in union_2]
NodepOfDep.union_3 [lemma, in union_3]
node_is_heap [constructor, in node_is_heap]
NoDup [inductive, in NoDup]
NoDupA [inductive, in NoDupA]
NoDupA_swap [lemma, in NoDupA_swap]
NoDupA_equivlistA_permut [lemma, in NoDupA_equivlistA_permut]
NoDupA_app [lemma, in NoDupA_app]
NoDupA_split [lemma, in NoDupA_split]
NoDupA_nil [constructor, in NoDupA_nil]
NoDupA_rev [lemma, in NoDupA_rev]
NoDupA_equivlistA_PermutationA [lemma, in NoDupA_equivlistA_PermutationA]
NoDupA_cons [constructor, in NoDupA_cons]
NoDupA_altdef [lemma, in NoDupA_altdef]
NoDupA_singleton [lemma, in NoDupA_singleton]
NoDup_cons [constructor, in NoDup_cons]
NoDup_Permutation [lemma, in NoDup_Permutation]
NoDup_remove_2 [lemma, in NoDup_remove_2]
NoDup_nil [constructor, in NoDup_nil]
NoDup_remove_1 [lemma, in NoDup_remove_1]
NoDup_permut [lemma, in NoDup_permut]
Noetherian [definition, in Noetherian]
noetherian [inductive, in noetherian]
Noetherian_contains_Noetherian [lemma, in Noetherian_contains_Noetherian]
None [constructor, in None]
nonneg [projection, in nonneg]
nonnegreal [record, in nonnegreal]
nonneg_derivative_1 [lemma, in nonneg_derivative_1]
nonneg_derivative_0 [lemma, in nonneg_derivative_0]
nonpos [projection, in nonpos]
nonposreal [record, in nonposreal]
nonpos_derivative_1 [lemma, in nonpos_derivative_1]
nonpos_derivative_0 [lemma, in nonpos_derivative_0]
nonzero [projection, in nonzero]
nonzeroreal [record, in nonzeroreal]
Non_disjoint_union' [lemma, in Non_disjoint_union']
non_dep_dep_functional_choice [lemma, in non_dep_dep_functional_choice]
non_dep_dep_functional_rel_reification [lemma, in non_dep_dep_functional_rel_reification]
Non_disjoint_union [lemma, in Non_disjoint_union]
Noone_in_empty [lemma, in Noone_in_empty]
Nop [module, in Nop]
NOrder [library]
NOrderProp [module, in NOrderProp]
NOrderProp.eq_0_gt_0_cases [lemma, in eq_0_gt_0_cases]
NOrderProp.le_pred_le_succ [lemma, in le_pred_le_succ]
NOrderProp.le_le_pred [lemma, in le_le_pred]
NOrderProp.le_ind_rel [lemma, in le_ind_rel]
NOrderProp.le_1_r [lemma, in le_1_r]
NOrderProp.le_0_r [lemma, in le_0_r]
NOrderProp.le_pred_le [lemma, in le_pred_le]
NOrderProp.le_succ_le_pred [lemma, in le_succ_le_pred]
NOrderProp.le_pred_l [lemma, in le_pred_l]
NOrderProp.lt_1_l' [lemma, in lt_1_l']
NOrderProp.lt_1_r [lemma, in lt_1_r]
NOrderProp.lt_pred_le [lemma, in lt_pred_le]
NOrderProp.lt_pred_l [lemma, in lt_pred_l]
NOrderProp.lt_pred_lt [lemma, in lt_pred_lt]
NOrderProp.lt_le_pred [lemma, in lt_le_pred]
NOrderProp.lt_lt_0 [lemma, in lt_lt_0]
NOrderProp.lt_succ_lt_pred [lemma, in lt_succ_lt_pred]
NOrderProp.lt_ind_rel [lemma, in lt_ind_rel]
NOrderProp.lt_0_succ [lemma, in lt_0_succ]
NOrderProp.lt_lt_pred [lemma, in lt_lt_pred]
NOrderProp.lt_wf_0 [lemma, in lt_wf_0]
NOrderProp.lt_pred_lt_succ [lemma, in lt_pred_lt_succ]
NOrderProp.neq_0_lt_0 [lemma, in neq_0_lt_0]
NOrderProp.nle_succ_0 [lemma, in nle_succ_0]
NOrderProp.nlt_0_r [lemma, in nlt_0_r]
NOrderProp.pred_lt_mono [lemma, in pred_lt_mono]
NOrderProp.pred_le_mono [lemma, in pred_le_mono]
NOrderProp.RelElim [section, in RelElim]
NOrderProp.RelElim.R [variable, in R]
NOrderProp.RelElim.R_wd [variable, in R_wd]
NOrderProp.succ_pred_pos [lemma, in succ_pred_pos]
NOrderProp.zero_one [lemma, in zero_one]
normalization_done [inductive, in normalization_done]
normalizes [projection, in normalizes]
normalizes [constructor, in normalizes]
Normalizes [record, in Normalizes]
Normalizes [inductive, in Normalizes]
Nor_semantics [lemma, in Nor_semantics]
not [definition, in not]
Notations [library]
notT [definition, in notT]
notzerop [definition, in notzerop]
notzerop_bool [definition, in notzerop_bool]
not_and_or [lemma, in not_and_or]
not_Zeq_inf [lemma, in not_Zeq_inf]
not_prime_divide [lemma, in not_prime_divide]
not_gt [lemma, in not_gt]
not_not_classic_set [lemma, in not_not_classic_set]
not_O_IZR [abbreviation, in not_O_IZR]
not_and [lemma, in not_and]
not_0_INR [lemma, in not_0_INR]
not_injective_elim [lemma, in not_injective_elim]
not_iff [lemma, in not_iff]
not_eq_false_beq [definition, in not_eq_false_beq]
not_imply_elim [lemma, in not_imply_elim]
not_Zeq [lemma, in not_Zeq]
not_not_iff [lemma, in not_not_iff]
not_imp_iff [lemma, in not_imp_iff]
not_INR [lemma, in not_INR]
not_identity_sym [lemma, in not_identity_sym]
not_included_empty_Inhabited [lemma, in not_included_empty_Inhabited]
not_imp_rev_iff [lemma, in not_imp_rev_iff]
not_or_and [lemma, in not_or_and]
not_nm_INR [abbreviation, in not_nm_INR]
not_0_IZR [lemma, in not_0_IZR]
not_1_INR [lemma, in not_1_INR]
not_has_fixpoint [lemma, in not_has_fixpoint]
Not_b [definition, in Not_b]
not_Rlt [lemma, in not_Rlt]
not_even_and_odd [lemma, in not_even_and_odd]
not_SIncl_empty [lemma, in not_SIncl_empty]
not_iff_morphism [instance, in not_iff_morphism]
not_imply_elim2 [lemma, in not_imply_elim2]
not_or [lemma, in not_or]
not_INR_O [abbreviation, in not_INR_O]
not_Empty_Add [lemma, in not_Empty_Add]
not_impl_morphism [instance, in not_impl_morphism]
not_or_iff [lemma, in not_or_iff]
not_false_iff [lemma, in not_false_iff]
not_true_iff [lemma, in not_true_iff]
not_prime_1 [lemma, in not_prime_1]
not_le [lemma, in not_le]
not_Zne [lemma, in not_Zne]
not_false_iff_true [lemma, in not_false_iff_true]
not_not_archimedean [lemma, in not_not_archimedean]
not_ex_not_all [lemma, in not_ex_not_all]
not_ex_not_all [lemma, in not_ex_not_all]
not_false_is_true [lemma, in not_false_is_true]
not_lt [lemma, in not_lt]
not_eq_sym [abbreviation, in not_eq_sym]
not_eq_sym [lemma, in not_eq_sym]
not_eq [lemma, in not_eq]
not_prime_0 [lemma, in not_prime_0]
not_all_not_ex [lemma, in not_all_not_ex]
not_all_not_ex [lemma, in not_all_not_ex]
not_empty_Inhabited [lemma, in not_empty_Inhabited]
not_not [lemma, in not_not]
not_all_ex_not [lemma, in not_all_ex_not]
not_all_ex_not [lemma, in not_all_ex_not]
not_imp [lemma, in not_imp]
not_eq_S [lemma, in not_eq_S]
not_ex_all_not [lemma, in not_ex_all_not]
not_ex_all_not [lemma, in not_ex_all_not]
not_rel_prime_0 [lemma, in not_rel_prime_0]
not_true_is_false [lemma, in not_true_is_false]
not_and_iff [lemma, in not_and_iff]
not_O_INR [abbreviation, in not_O_INR]
not_ge [lemma, in not_ge]
not_true_iff_false [lemma, in not_true_iff_false]
not_le_minus_0 [lemma, in not_le_minus_0]
no_cond [definition, in no_cond]
no_fixpoint_negb [lemma, in no_fixpoint_negb]
NParity [library]
NParityProp [module, in NParityProp]
NParityProp.even_sub [lemma, in even_sub]
NParityProp.even_pred [lemma, in even_pred]
NParityProp.odd_sub [lemma, in odd_sub]
NParityProp.odd_pred [lemma, in odd_pred]
Npdist [definition, in Npdist]
Npdist_eq_1 [lemma, in Npdist_eq_1]
Npdist_comm [lemma, in Npdist_comm]
Npdist_ultra [lemma, in Npdist_ultra]
Npdist_eq_2 [lemma, in Npdist_eq_2]
NPeano [library]
Nplength [definition, in Nplength]
Nplength_first_one [lemma, in Nplength_first_one]
Nplength_infty [lemma, in Nplength_infty]
Nplength_ultra_1 [lemma, in Nplength_ultra_1]
Nplength_lb [lemma, in Nplength_lb]
Nplength_zeros [lemma, in Nplength_zeros]
Nplength_ub [lemma, in Nplength_ub]
Nplength_one [lemma, in Nplength_one]
Nplength_ultra [lemma, in Nplength_ultra]
Nplus [abbreviation, in Nplus]
Nplus_comm [abbreviation, in Nplus_comm]
Nplus_reg_l [lemma, in Nplus_reg_l]
Nplus_0_l [abbreviation, in Nplus_0_l]
Nplus_assoc [abbreviation, in Nplus_assoc]
Nplus_succ [abbreviation, in Nplus_succ]
Nplus_0_r [abbreviation, in Nplus_0_r]
Npos [constructor, in Npos]
Npos [abbreviation, in Npos]
Npow [abbreviation, in Npow]
NPow [library]
NPowProp [module, in NPowProp]
NPowProp.even_pow [lemma, in even_pow]
NPowProp.odd_pow [lemma, in odd_pow]
NPowProp.pow_le_mono_r [lemma, in pow_le_mono_r]
NPowProp.pow_inj_l [lemma, in pow_inj_l]
NPowProp.pow_lt_mono [definition, in pow_lt_mono]
NPowProp.pow_le_mono_l_iff [lemma, in pow_le_mono_l_iff]
NPowProp.pow_nonzero [lemma, in pow_nonzero]
NPowProp.pow_lt_mono_l [lemma, in pow_lt_mono_l]
NPowProp.pow_le_mono_r_iff [lemma, in pow_le_mono_r_iff]
NPowProp.pow_le_mono_l [lemma, in pow_le_mono_l]
NPowProp.pow_gt_lin_r [lemma, in pow_gt_lin_r]
NPowProp.pow_1_l [lemma, in pow_1_l]
NPowProp.pow_0_l [lemma, in pow_0_l]
NPowProp.pow_mul_r [lemma, in pow_mul_r]
NPowProp.pow_add_r [lemma, in pow_add_r]
NPowProp.pow_1_r [definition, in pow_1_r]
NPowProp.pow_lt_mono_r_iff [lemma, in pow_lt_mono_r_iff]
NPowProp.pow_2_r [definition, in pow_2_r]
NPowProp.pow_lt_mono_l_iff [lemma, in pow_lt_mono_l_iff]
NPowProp.pow_eq_0_iff [lemma, in pow_eq_0_iff]
NPowProp.pow_add_upper [lemma, in pow_add_upper]
NPowProp.pow_le_mono [lemma, in pow_le_mono]
NPowProp.pow_eq_0 [lemma, in pow_eq_0]
NPowProp.pow_add_lower [lemma, in pow_add_lower]
NPowProp.pow_gt_1 [lemma, in pow_gt_1]
NPowProp.pow_mul_l [lemma, in pow_mul_l]
NPowProp.pow_inj_r [lemma, in pow_inj_r]
NPowProp.pow_succ_r' [lemma, in pow_succ_r']
NPowProp.pow_lt_mono_r [lemma, in pow_lt_mono_r]
NPowProp.Private_NZPow [module, in NPowProp.Private_NZPow]
Npow_succ_r [abbreviation, in Npow_succ_r]
Npow_0_r [abbreviation, in Npow_0_r]
Npred [abbreviation, in Npred]
Npred_succ [abbreviation, in Npred_succ]
Npred_minus [abbreviation, in Npred_minus]
nprod [definition, in nprod]
nprod_of_list [definition, in nprod_of_list]
nprod_to_list [definition, in nprod_to_list]
NProp [module, in NProp]
NProperties [library]
Nrec [abbreviation, in Nrec]
Nrect [abbreviation, in Nrect]
Nrect_step [abbreviation, in Nrect_step]
Nrect_base [abbreviation, in Nrect_base]
Nrec_base [abbreviation, in Nrec_base]
Nrec_succ [abbreviation, in Nrec_succ]
Nsame_bit0 [lemma, in Nsame_bit0]
nshiftl [definition, in nshiftl]
Nshiftl_nat_S [lemma, in Nshiftl_nat_S]
nshiftl_n_0 [lemma, in nshiftl_n_0]
Nshiftl_nat_spec_low [lemma, in Nshiftl_nat_spec_low]
nshiftl_size [lemma, in nshiftl_size]
nshiftl_above_size [lemma, in nshiftl_above_size]
Nshiftl_nat_equiv [lemma, in Nshiftl_nat_equiv]
Nshiftl_nat_spec_high [lemma, in Nshiftl_nat_spec_high]
nshiftl_S_tail [lemma, in nshiftl_S_tail]
nshiftl_S [lemma, in nshiftl_S]
Nshiftl_equiv_nat [lemma, in Nshiftl_equiv_nat]
nshiftr [definition, in nshiftr]
nshiftr_S_tail [lemma, in nshiftr_S_tail]
nshiftr_n_0 [lemma, in nshiftr_n_0]
Nshiftr_equiv_nat [lemma, in Nshiftr_equiv_nat]
Nshiftr_nat_equiv [lemma, in Nshiftr_nat_equiv]
nshiftr_S [lemma, in nshiftr_S]
nshiftr_predsize_0_firstl [lemma, in nshiftr_predsize_0_firstl]
Nshiftr_nat_spec [lemma, in Nshiftr_nat_spec]
Nshiftr_nat_S [lemma, in Nshiftr_nat_S]
nshiftr_size [lemma, in nshiftr_size]
nshiftr_above_size [lemma, in nshiftr_above_size]
nshiftr_0_propagates [lemma, in nshiftr_0_propagates]
nshiftr_0_firstl [lemma, in nshiftr_0_firstl]
NSig [library]
NSigNAxioms [library]
Nsize [abbreviation, in Nsize]
Nsqrt [abbreviation, in Nsqrt]
NSqrt [library]
NSqrtProp [module, in NSqrtProp]
NSqrtProp.add_sqrt_le [lemma, in add_sqrt_le]
NSqrtProp.Private_NZSqrt [module, in NSqrtProp.Private_NZSqrt]
NSqrtProp.sqrt_unique [definition, in sqrt_unique]
NSqrtProp.sqrt_le_mono [definition, in sqrt_le_mono]
NSqrtProp.sqrt_mul_below [definition, in sqrt_mul_below]
NSqrtProp.sqrt_le_lin [lemma, in sqrt_le_lin]
NSqrtProp.sqrt_1 [definition, in sqrt_1]
NSqrtProp.sqrt_0 [definition, in sqrt_0]
NSqrtProp.sqrt_lt_cancel [definition, in sqrt_lt_cancel]
NSqrtProp.sqrt_succ_le [lemma, in sqrt_succ_le]
NSqrtProp.sqrt_le_square [lemma, in sqrt_le_square]
NSqrtProp.sqrt_succ_or [lemma, in sqrt_succ_or]
NSqrtProp.sqrt_add_le [definition, in sqrt_add_le]
NSqrtProp.sqrt_2 [definition, in sqrt_2]
NSqrtProp.sqrt_lt_square [lemma, in sqrt_lt_square]
NSqrtProp.sqrt_lt_lin [definition, in sqrt_lt_lin]
NSqrtProp.sqrt_spec' [lemma, in sqrt_spec']
NSqrtProp.sqrt_mul_above [lemma, in sqrt_mul_above]
NSqrtProp.sqrt_square [lemma, in sqrt_square]
Nsqrtrem [abbreviation, in Nsqrtrem]
Nsqrtrem_spec [abbreviation, in Nsqrtrem_spec]
Nsqrtrem_sqrt [abbreviation, in Nsqrtrem_sqrt]
Nsqrt_spec [abbreviation, in Nsqrt_spec]
Nsqrt_def [library]
NStrongRec [library]
NStrongRecProp [module, in NStrongRecProp]
NStrongRecProp.StrongRecursion [section, in StrongRecursion]
NStrongRecProp.StrongRecursion.A [variable, in A]
NStrongRecProp.StrongRecursion.Aeq [variable, in Aeq]
NStrongRecProp.StrongRecursion.Aeq_equiv [variable, in Aeq_equiv]
NStrongRecProp.StrongRecursion.FixPoint [section, in FixPoint]
NStrongRecProp.StrongRecursion.FixPoint.f [variable, in f]
NStrongRecProp.StrongRecursion.FixPoint.f_wd [variable, in f_wd]
NStrongRecProp.StrongRecursion.FixPoint.step_good [variable, in step_good]
NStrongRecProp.strong_rec_0 [lemma, in strong_rec_0]
NStrongRecProp.strong_rec [definition, in strong_rec]
NStrongRecProp.strong_rec0 [definition, in strong_rec0]
NStrongRecProp.strong_rec_alt [lemma, in strong_rec_alt]
NStrongRecProp.strong_rec0_succ [lemma, in strong_rec0_succ]
NStrongRecProp.strong_rec0_0 [lemma, in strong_rec0_0]
NStrongRecProp.strong_rec0_more_steps [lemma, in strong_rec0_more_steps]
NStrongRecProp.strong_rec_fixpoint [lemma, in strong_rec_fixpoint]
NStrongRecProp.strong_rec0_fixpoint [lemma, in strong_rec0_fixpoint]
NStrongRecProp.strong_rec0_wd [instance, in strong_rec0_wd]
NStrongRecProp.strong_rec_0_any [lemma, in strong_rec_0_any]
NStrongRecProp.strong_rec_any_fst_arg [lemma, in strong_rec_any_fst_arg]
NStrongRecProp.strong_rec_wd [instance, in strong_rec_wd]
NSub [library]
NSubProp [module, in NSubProp]
NSubProp.add_sub_assoc [lemma, in add_sub_assoc]
NSubProp.add_dichotomy [lemma, in add_dichotomy]
NSubProp.add_sub_swap [lemma, in add_sub_swap]
NSubProp.add_sub_eq_nz [lemma, in add_sub_eq_nz]
NSubProp.add_sub_eq_l [lemma, in add_sub_eq_l]
NSubProp.add_sub [lemma, in add_sub]
NSubProp.add_sub_eq_r [lemma, in add_sub_eq_r]
NSubProp.le_add_le_sub_r [lemma, in le_add_le_sub_r]
NSubProp.le_equiv [lemma, in le_equiv]
NSubProp.le_sub_le_add_l [lemma, in le_sub_le_add_l]
NSubProp.le_alt [definition, in le_alt]
NSubProp.le_alt_wd [instance, in le_alt_wd]
NSubProp.le_sub_l [lemma, in le_sub_l]
NSubProp.le_sub_le_add_r [lemma, in le_sub_le_add_r]
NSubProp.le_add_le_sub_l [lemma, in le_add_le_sub_l]
NSubProp.le_alt_dichotomy [lemma, in le_alt_dichotomy]
NSubProp.lt_sub_lt_add_r [lemma, in lt_sub_lt_add_r]
NSubProp.lt_equiv [lemma, in lt_equiv]
NSubProp.lt_add_lt_sub_r [lemma, in lt_add_lt_sub_r]
NSubProp.lt_add_lt_sub_l [lemma, in lt_add_lt_sub_l]
NSubProp.lt_alt_wd [instance, in lt_alt_wd]
NSubProp.lt_alt [definition, in lt_alt]
NSubProp.lt_sub_lt_add_l [lemma, in lt_sub_lt_add_l]
NSubProp.mul_sub_distr_r [lemma, in mul_sub_distr_r]
NSubProp.mul_pred_r [lemma, in mul_pred_r]
NSubProp.mul_sub_distr_l [lemma, in mul_sub_distr_l]
NSubProp.sub_le_mono_l [lemma, in sub_le_mono_l]
NSubProp.sub_gt [lemma, in sub_gt]
NSubProp.sub_0_l [lemma, in sub_0_l]
NSubProp.sub_le_mono_r [lemma, in sub_le_mono_r]
NSubProp.sub_succ_l [lemma, in sub_succ_l]
NSubProp.sub_0_le [lemma, in sub_0_le]
NSubProp.sub_add [lemma, in sub_add]
NSubProp.sub_succ [lemma, in sub_succ]
NSubProp.sub_diag [lemma, in sub_diag]
NSubProp.sub_add_le [lemma, in sub_add_le]
NSubProp.sub_lt [lemma, in sub_lt]
NSubProp.sub_add_distr [lemma, in sub_add_distr]
Nsucc [abbreviation, in Nsucc]
Nsucc_pos_spec [abbreviation, in Nsucc_pos_spec]
Nsucc_0 [abbreviation, in Nsucc_0]
Nsucc_pred [abbreviation, in Nsucc_pred]
Nsucc_inj [abbreviation, in Nsucc_inj]
Nsucc_pos [abbreviation, in Nsucc_pos]
Ntestbit_Nbit [lemma, in Ntestbit_Nbit]
nth [definition, in nth]
nth [definition, in nth]
ntheq_eqst [lemma, in ntheq_eqst]
nth_indep [lemma, in nth_indep]
nth_S [constructor, in nth_S]
nth_In [lemma, in nth_In]
nth_S_cons [lemma, in nth_S_cons]
nth_ok [definition, in nth_ok]
nth_map [lemma, in nth_map]
nth_order [definition, in nth_order]
nth_error [definition, in nth_error]
nth_default_eq [lemma, in nth_default_eq]
nth_order_last [lemma, in nth_order_last]
nth_map2 [lemma, in nth_map2]
nth_O [constructor, in nth_O]
nth_le [lemma, in nth_le]
nth_in_or_default [lemma, in nth_in_or_default]
nth_default [definition, in nth_default]
nth_overflow [lemma, in nth_overflow]
NType [module, in NType]
NTypeIsNAxioms [module, in NTypeIsNAxioms]
NTypeIsNAxioms.add_succ_l [lemma, in add_succ_l]
NTypeIsNAxioms.add_0_l [lemma, in add_0_l]
NTypeIsNAxioms.add_wd [instance, in add_wd]
NTypeIsNAxioms.bi_induction [lemma, in bi_induction]
NTypeIsNAxioms.BS [lemma, in BS]
NTypeIsNAxioms.B_holds [lemma, in B_holds]
NTypeIsNAxioms.B0 [lemma, in B0]
NTypeIsNAxioms.compare_lt_iff [lemma, in compare_lt_iff]
NTypeIsNAxioms.compare_antisym [lemma, in compare_antisym]
NTypeIsNAxioms.compare_le_iff [lemma, in compare_le_iff]
NTypeIsNAxioms.compare_eq_iff [lemma, in compare_eq_iff]
NTypeIsNAxioms.compare_wd [instance, in compare_wd]
NTypeIsNAxioms.divide [definition, in divide]
NTypeIsNAxioms.div_wd [instance, in div_wd]
NTypeIsNAxioms.div_mod [lemma, in div_mod]
NTypeIsNAxioms.div2_spec [lemma, in div2_spec]
NTypeIsNAxioms.eqb_eq [lemma, in eqb_eq]
NTypeIsNAxioms.eqb_wd [instance, in eqb_wd]
NTypeIsNAxioms.eq_equiv [instance, in eq_equiv]
NTypeIsNAxioms.Even [definition, in Even]
NTypeIsNAxioms.even_spec [lemma, in even_spec]
NTypeIsNAxioms.gcd_nonneg [lemma, in gcd_nonneg]
NTypeIsNAxioms.gcd_greatest [lemma, in gcd_greatest]
NTypeIsNAxioms.gcd_divide_r [lemma, in gcd_divide_r]
NTypeIsNAxioms.gcd_divide_l [lemma, in gcd_divide_l]
NTypeIsNAxioms.Induction [section, in Induction]
NTypeIsNAxioms.Induction.A [variable, in A]
NTypeIsNAxioms.Induction.AS [variable, in AS]
NTypeIsNAxioms.Induction.A_wd [variable, in A_wd]
NTypeIsNAxioms.Induction.A0 [variable, in A0]
NTypeIsNAxioms.Induction.B [variable, in B]
NTypeIsNAxioms.land_spec [lemma, in land_spec]
NTypeIsNAxioms.ldiff_spec [lemma, in ldiff_spec]
NTypeIsNAxioms.leb_le [lemma, in leb_le]
NTypeIsNAxioms.leb_wd [instance, in leb_wd]
NTypeIsNAxioms.log2_spec [lemma, in log2_spec]
NTypeIsNAxioms.log2_nonpos [lemma, in log2_nonpos]
NTypeIsNAxioms.lor_spec [lemma, in lor_spec]
NTypeIsNAxioms.ltb_wd [instance, in ltb_wd]
NTypeIsNAxioms.ltb_lt [lemma, in ltb_lt]
NTypeIsNAxioms.lt_succ_r [lemma, in lt_succ_r]
NTypeIsNAxioms.lt_wd [instance, in lt_wd]
NTypeIsNAxioms.lxor_spec [lemma, in lxor_spec]
NTypeIsNAxioms.max_r [lemma, in max_r]
NTypeIsNAxioms.max_l [lemma, in max_l]
NTypeIsNAxioms.min_r [lemma, in min_r]
NTypeIsNAxioms.min_l [lemma, in min_l]
NTypeIsNAxioms.mod_bound_pos [lemma, in mod_bound_pos]
NTypeIsNAxioms.mod_wd [instance, in mod_wd]
NTypeIsNAxioms.mul_succ_l [lemma, in mul_succ_l]
NTypeIsNAxioms.mul_0_l [lemma, in mul_0_l]
NTypeIsNAxioms.mul_wd [instance, in mul_wd]
NTypeIsNAxioms.N_of_Z [definition, in N_of_Z]
NTypeIsNAxioms.Odd [definition, in Odd]
NTypeIsNAxioms.odd_spec [lemma, in odd_spec]
NTypeIsNAxioms.one_succ [lemma, in one_succ]
NTypeIsNAxioms.pow_wd [instance, in pow_wd]
NTypeIsNAxioms.pow_pow_N [lemma, in pow_pow_N]
NTypeIsNAxioms.pow_0_r [lemma, in pow_0_r]
NTypeIsNAxioms.pow_pos_N [lemma, in pow_pos_N]
NTypeIsNAxioms.pow_succ_r [lemma, in pow_succ_r]
NTypeIsNAxioms.pow_N_pow [lemma, in pow_N_pow]
NTypeIsNAxioms.pow_neg_r [lemma, in pow_neg_r]
NTypeIsNAxioms.pred_succ [lemma, in pred_succ]
NTypeIsNAxioms.pred_0 [lemma, in pred_0]
NTypeIsNAxioms.pred_wd [instance, in pred_wd]
NTypeIsNAxioms.recursion [definition, in recursion]
NTypeIsNAxioms.recursion_wd [instance, in recursion_wd]
NTypeIsNAxioms.recursion_0 [lemma, in recursion_0]
NTypeIsNAxioms.recursion_succ [lemma, in recursion_succ]
NTypeIsNAxioms.shiftl_spec_low [lemma, in shiftl_spec_low]
NTypeIsNAxioms.shiftl_spec_high [lemma, in shiftl_spec_high]
NTypeIsNAxioms.shiftr_spec [lemma, in shiftr_spec]
NTypeIsNAxioms.spec_divide [lemma, in spec_divide]
NTypeIsNAxioms.spec_N_of_Z [lemma, in spec_N_of_Z]
NTypeIsNAxioms.sqrt_spec [lemma, in sqrt_spec]
NTypeIsNAxioms.sqrt_neg [lemma, in sqrt_neg]
NTypeIsNAxioms.square_spec [lemma, in square_spec]
NTypeIsNAxioms.sub_wd [instance, in sub_wd]
NTypeIsNAxioms.sub_succ_r [lemma, in sub_succ_r]
NTypeIsNAxioms.sub_0_r [lemma, in sub_0_r]
NTypeIsNAxioms.succ_wd [instance, in succ_wd]
NTypeIsNAxioms.testbit_even_0 [lemma, in testbit_even_0]
NTypeIsNAxioms.testbit_neg_r [lemma, in testbit_neg_r]
NTypeIsNAxioms.testbit_even_succ [lemma, in testbit_even_succ]
NTypeIsNAxioms.testbit_odd_0 [lemma, in testbit_odd_0]
NTypeIsNAxioms.testbit_odd_succ [lemma, in testbit_odd_succ]
NTypeIsNAxioms.testbit_wd [instance, in testbit_wd]
NTypeIsNAxioms.two_succ [lemma, in two_succ]
( _ | _ ) [notation, in ::'('_x_'|'_x_')']
NType_ZType.Zabs_N [axiom, in Zabs_N]
_ ^ _ [notation, in ::x_'^'_x]
_ < _ [notation, in ::x_'<'_x]
NType_ZType.spec_Zabs_N [axiom, in spec_Zabs_N]
NType_ZType.Z_of_N [axiom, in Z_of_N]
NType_ZType.spec_Z_of_N [axiom, in spec_Z_of_N]
NType_ZType [module, in NType_ZType]
_ == _ [notation, in ::x_'=='_x]
NType_Notation [module, in NType_Notation]
2 [notation, in ::'2']
[ _ ] [notation, in ::'['_x_']']
_ - _ [notation, in ::x_'-'_x]
1 [notation, in ::'1']
_ * _ [notation, in ::x_'*'_x]
_ <= _ [notation, in ::x_'<='_x]
NType_NAxioms [module, in NType_NAxioms]
_ + _ [notation, in ::x_'+'_x]
0 [notation, in ::'0']
NType' [module, in NType']
NType.add [axiom, in add]
NType.compare [axiom, in compare]
NType.div [axiom, in div]
NType.div_eucl [axiom, in div_eucl]
NType.div2 [axiom, in div2]
NType.eq [definition, in eq]
NType.eqb [axiom, in eqb]
NType.even [axiom, in even]
NType.gcd [axiom, in gcd]
NType.land [axiom, in land]
NType.ldiff [axiom, in ldiff]
NType.le [definition, in le]
NType.leb [axiom, in leb]
NType.log2 [axiom, in log2]
NType.lor [axiom, in lor]
NType.lt [definition, in lt]
NType.ltb [axiom, in ltb]
NType.lxor [axiom, in lxor]
NType.max [axiom, in max]
NType.min [axiom, in min]
NType.modulo [axiom, in modulo]
NType.mul [axiom, in mul]
NType.odd [axiom, in odd]
NType.of_N [axiom, in of_N]
NType.one [axiom, in one]
NType.pow [axiom, in pow]
NType.pow_N [axiom, in pow_N]
NType.pow_pos [axiom, in pow_pos]
NType.pred [axiom, in pred]
NType.shiftl [axiom, in shiftl]
NType.shiftr [axiom, in shiftr]
NType.spec_ltb [axiom, in spec_ltb]
NType.spec_shiftl [axiom, in spec_shiftl]
NType.spec_pos [axiom, in spec_pos]
NType.spec_pred [axiom, in spec_pred]
NType.spec_max [axiom, in spec_max]
NType.spec_leb [axiom, in spec_leb]
NType.spec_add [axiom, in spec_add]
NType.spec_land [axiom, in spec_land]
NType.spec_odd [axiom, in spec_odd]
NType.spec_shiftr [axiom, in spec_shiftr]
NType.spec_2 [axiom, in spec_2]
NType.spec_div2 [axiom, in spec_div2]
NType.spec_mul [axiom, in spec_mul]
NType.spec_testbit [axiom, in spec_testbit]
NType.spec_1 [axiom, in spec_1]
NType.spec_eqb [axiom, in spec_eqb]
NType.spec_lxor [axiom, in spec_lxor]
NType.spec_modulo [axiom, in spec_modulo]
NType.spec_compare [axiom, in spec_compare]
NType.spec_pow [axiom, in spec_pow]
NType.spec_even [axiom, in spec_even]
NType.spec_ldiff [axiom, in spec_ldiff]
NType.spec_div [axiom, in spec_div]
NType.spec_div_eucl [axiom, in spec_div_eucl]
NType.spec_pow_pos [axiom, in spec_pow_pos]
NType.spec_lor [axiom, in spec_lor]
NType.spec_sub [axiom, in spec_sub]
NType.spec_succ [axiom, in spec_succ]
NType.spec_sqrt [axiom, in spec_sqrt]
NType.spec_min [axiom, in spec_min]
NType.spec_log2 [axiom, in spec_log2]
NType.spec_gcd [axiom, in spec_gcd]
NType.spec_pow_N [axiom, in spec_pow_N]
NType.spec_square [axiom, in spec_square]
NType.spec_of_N [axiom, in spec_of_N]
NType.spec_0 [axiom, in spec_0]
NType.sqrt [axiom, in sqrt]
NType.square [axiom, in square]
NType.sub [axiom, in sub]
NType.succ [axiom, in succ]
NType.t [axiom, in t]
NType.testbit [axiom, in testbit]
NType.to_N [definition, in to_N]
NType.to_Z [axiom, in to_Z]
NType.two [axiom, in two]
NType.zero [axiom, in zero]
[ _ ] [notation, in ::'['_x_']']
null_derivative_1 [lemma, in null_derivative_1]
null_derivative_loc [lemma, in null_derivative_loc]
null_derivative_0 [lemma, in null_derivative_0]
NumPrelude [library]
nuncurry [definition, in nuncurry]
nu_left_inv [lemma, in nu_left_inv]
Nxor [abbreviation, in Nxor]
Nxor_neutral_right [abbreviation, in Nxor_neutral_right]
Nxor_eq_false [lemma, in Nxor_eq_false]
Nxor_semantics [lemma, in Nxor_semantics]
Nxor_assoc [abbreviation, in Nxor_assoc]
Nxor_bit0 [lemma, in Nxor_bit0]
Nxor_comm [abbreviation, in Nxor_comm]
Nxor_BVxor [lemma, in Nxor_BVxor]
Nxor_eq_true [lemma, in Nxor_eq_true]
Nxor_div2 [lemma, in Nxor_div2]
Nxor_eq [abbreviation, in Nxor_eq]
Nxor_nilpotent [abbreviation, in Nxor_nilpotent]
Nxor_neutral_left [abbreviation, in Nxor_neutral_left]
NZAdd [library]
NZAddOrder [library]
NZAddOrderProp [module, in NZAddOrderProp]
NZAddOrderProp.add_lt_cases [lemma, in add_lt_cases]
NZAddOrderProp.add_nonneg_cases [lemma, in add_nonneg_cases]
NZAddOrderProp.add_pos_nonneg [lemma, in add_pos_nonneg]
NZAddOrderProp.add_le_cases [lemma, in add_le_cases]
NZAddOrderProp.add_nonpos_cases [lemma, in add_nonpos_cases]
NZAddOrderProp.add_lt_mono [lemma, in add_lt_mono]
NZAddOrderProp.add_le_mono_r [lemma, in add_le_mono_r]
NZAddOrderProp.add_lt_le_mono [lemma, in add_lt_le_mono]
NZAddOrderProp.add_nonneg_nonneg [lemma, in add_nonneg_nonneg]
NZAddOrderProp.add_neg_cases [lemma, in add_neg_cases]
NZAddOrderProp.add_pos_pos [lemma, in add_pos_pos]
NZAddOrderProp.add_nonneg_pos [lemma, in add_nonneg_pos]
NZAddOrderProp.add_lt_mono_l [lemma, in add_lt_mono_l]
NZAddOrderProp.add_le_mono_l [lemma, in add_le_mono_l]
NZAddOrderProp.add_le_lt_mono [lemma, in add_le_lt_mono]
NZAddOrderProp.add_le_mono [lemma, in add_le_mono]
NZAddOrderProp.add_pos_cases [lemma, in add_pos_cases]
NZAddOrderProp.add_lt_mono_r [lemma, in add_lt_mono_r]
NZAddOrderProp.le_lt_add_lt [lemma, in le_lt_add_lt]
NZAddOrderProp.le_le_add_le [lemma, in le_le_add_le]
NZAddOrderProp.le_exists_sub [lemma, in le_exists_sub]
NZAddOrderProp.lt_add_pos_l [lemma, in lt_add_pos_l]
NZAddOrderProp.lt_le_add_lt [lemma, in lt_le_add_lt]
NZAddOrderProp.lt_add_pos_r [lemma, in lt_add_pos_r]
NZAddProp [module, in NZAddProp]
NZAddProp.add_1_r [lemma, in add_1_r]
NZAddProp.add_shuffle0 [lemma, in add_shuffle0]
NZAddProp.add_succ_r [lemma, in add_succ_r]
NZAddProp.add_cancel_l [lemma, in add_cancel_l]
NZAddProp.add_0_r [lemma, in add_0_r]
NZAddProp.add_assoc [lemma, in add_assoc]
NZAddProp.add_comm [lemma, in add_comm]
NZAddProp.add_shuffle2 [lemma, in add_shuffle2]
NZAddProp.add_shuffle3 [lemma, in add_shuffle3]
NZAddProp.add_1_l [lemma, in add_1_l]
NZAddProp.add_cancel_r [lemma, in add_cancel_r]
NZAddProp.add_succ_comm [lemma, in add_succ_comm]
NZAddProp.add_shuffle1 [lemma, in add_shuffle1]
NZAddProp.sub_1_r [lemma, in sub_1_r]
NZAxioms [library]
NZAxiomsSig [module, in NZAxiomsSig]
NZAxiomsSig' [module, in NZAxiomsSig']
NZBase [library]
NZBaseProp [module, in NZBaseProp]
NZBaseProp.CentralInduction [section, in CentralInduction]
NZBaseProp.CentralInduction.A [variable, in A]
NZBaseProp.CentralInduction.A_wd [variable, in A_wd]
NZBaseProp.central_induction [lemma, in central_induction]
NZBaseProp.eq_sym_iff [lemma, in eq_sym_iff]
NZBaseProp.eq_stepl [lemma, in eq_stepl]
NZBaseProp.neq_sym [lemma, in neq_sym]
NZBaseProp.succ_inj [lemma, in succ_inj]
NZBaseProp.succ_inj_wd_neg [lemma, in succ_inj_wd_neg]
NZBaseProp.succ_inj_wd [lemma, in succ_inj_wd]
NZBasicFunsSig [module, in NZBasicFunsSig]
NZBasicFunsSig' [module, in NZBasicFunsSig']
NZBits [module, in NZBits]
NZBits [library]
NZBitsSpec [module, in NZBitsSpec]
NZBitsSpec.div2_spec [axiom, in div2_spec]
NZBitsSpec.land_spec [axiom, in land_spec]
NZBitsSpec.ldiff_spec [axiom, in ldiff_spec]
NZBitsSpec.lor_spec [axiom, in lor_spec]
NZBitsSpec.lxor_spec [axiom, in lxor_spec]
NZBitsSpec.shiftl_spec_low [axiom, in shiftl_spec_low]
NZBitsSpec.shiftl_spec_high [axiom, in shiftl_spec_high]
NZBitsSpec.shiftr_spec [axiom, in shiftr_spec]
NZBitsSpec.testbit_even_0 [axiom, in testbit_even_0]
NZBitsSpec.testbit_neg_r [axiom, in testbit_neg_r]
NZBitsSpec.testbit_even_succ [axiom, in testbit_even_succ]
NZBitsSpec.testbit_odd_0 [axiom, in testbit_odd_0]
NZBitsSpec.testbit_odd_succ [axiom, in testbit_odd_succ]
NZBitsSpec.testbit_wd [instance, in testbit_wd]
NZBits' [module, in NZBits']
NZCyclic [library]
NZCyclicAxiomsMod [module, in NZCyclicAxiomsMod]
NZCyclicAxiomsMod.add [definition, in add]
NZCyclicAxiomsMod.add_succ_l [lemma, in add_succ_l]
NZCyclicAxiomsMod.add_0_l [lemma, in add_0_l]
NZCyclicAxiomsMod.add_wd [instance, in add_wd]
NZCyclicAxiomsMod.bi_induction [lemma, in bi_induction]
NZCyclicAxiomsMod.BS [lemma, in BS]
NZCyclicAxiomsMod.B_holds [lemma, in B_holds]
NZCyclicAxiomsMod.B0 [lemma, in B0]
NZCyclicAxiomsMod.eq [definition, in eq]
NZCyclicAxiomsMod.eq_equiv [instance, in eq_equiv]
NZCyclicAxiomsMod.gt_wB_1 [lemma, in gt_wB_1]
NZCyclicAxiomsMod.gt_wB_0 [lemma, in gt_wB_0]
NZCyclicAxiomsMod.Induction [section, in Induction]
NZCyclicAxiomsMod.Induction.A [variable, in A]
NZCyclicAxiomsMod.Induction.AS [variable, in AS]
NZCyclicAxiomsMod.Induction.A_wd [variable, in A_wd]
NZCyclicAxiomsMod.Induction.A0 [variable, in A0]
NZCyclicAxiomsMod.Induction.B [variable, in B]
NZCyclicAxiomsMod.mul [definition, in mul]
NZCyclicAxiomsMod.mul_succ_l [lemma, in mul_succ_l]
NZCyclicAxiomsMod.mul_0_l [lemma, in mul_0_l]
NZCyclicAxiomsMod.mul_wd [instance, in mul_wd]
NZCyclicAxiomsMod.NZ_to_Z_mod [lemma, in NZ_to_Z_mod]
NZCyclicAxiomsMod.one [definition, in one]
NZCyclicAxiomsMod.one_mod_wB [lemma, in one_mod_wB]
NZCyclicAxiomsMod.one_succ [lemma, in one_succ]
NZCyclicAxiomsMod.P [abbreviation, in P]
NZCyclicAxiomsMod.pred [definition, in pred]
NZCyclicAxiomsMod.pred_mod_wB [lemma, in pred_mod_wB]
NZCyclicAxiomsMod.pred_succ [lemma, in pred_succ]
NZCyclicAxiomsMod.pred_wd [instance, in pred_wd]
NZCyclicAxiomsMod.S [abbreviation, in S]
NZCyclicAxiomsMod.sub [definition, in sub]
NZCyclicAxiomsMod.sub_wd [instance, in sub_wd]
NZCyclicAxiomsMod.sub_succ_r [lemma, in sub_succ_r]
NZCyclicAxiomsMod.sub_0_r [lemma, in sub_0_r]
NZCyclicAxiomsMod.succ [definition, in succ]
NZCyclicAxiomsMod.succ_mod_wB [lemma, in succ_mod_wB]
NZCyclicAxiomsMod.succ_wd [instance, in succ_wd]
NZCyclicAxiomsMod.t [definition, in t]
NZCyclicAxiomsMod.two [definition, in two]
NZCyclicAxiomsMod.two_succ [lemma, in two_succ]
NZCyclicAxiomsMod.wB [abbreviation, in wB]
NZCyclicAxiomsMod.zero [definition, in zero]
_ == _ [notation, in ::x_'=='_x]
_ - _ [notation, in ::x_'-'_x]
_ * _ [notation, in ::x_'*'_x]
_ + _ [notation, in ::x_'+'_x]
0 [notation, in ::'0']
[| _ |] [notation, in ::'[|'_x_'|]']
NZDecOrdAxiomsSig [module, in NZDecOrdAxiomsSig]
NZDecOrdAxiomsSig' [module, in NZDecOrdAxiomsSig']
NZDecOrdSig [module, in NZDecOrdSig]
NZDecOrdSig' [module, in NZDecOrdSig']
NZDiv [module, in NZDiv]
NZDiv [library]
NZDivProp [module, in NZDivProp]
NZDivProp.add_mod_idemp_r [lemma, in add_mod_idemp_r]
NZDivProp.add_mod_idemp_l [lemma, in add_mod_idemp_l]
NZDivProp.add_mod [lemma, in add_mod]
NZDivProp.div_mod_unique [lemma, in div_mod_unique]
NZDivProp.div_unique [lemma, in div_unique]
NZDivProp.div_small_iff [lemma, in div_small_iff]
NZDivProp.div_mul_le [lemma, in div_mul_le]
NZDivProp.div_mul [lemma, in div_mul]
NZDivProp.div_0_l [lemma, in div_0_l]
NZDivProp.div_div [lemma, in div_div]
NZDivProp.div_add [lemma, in div_add]
NZDivProp.div_1_l [lemma, in div_1_l]
NZDivProp.div_exact [lemma, in div_exact]
NZDivProp.div_le_mono [lemma, in div_le_mono]
NZDivProp.div_same [lemma, in div_same]
NZDivProp.div_pos [lemma, in div_pos]
NZDivProp.div_unique_exact [lemma, in div_unique_exact]
NZDivProp.div_mul_cancel_r [lemma, in div_mul_cancel_r]
NZDivProp.div_le_compat_l [lemma, in div_le_compat_l]
NZDivProp.div_le_upper_bound [lemma, in div_le_upper_bound]
NZDivProp.div_lt [lemma, in div_lt]
NZDivProp.div_mul_cancel_l [lemma, in div_mul_cancel_l]
NZDivProp.div_le_lower_bound [lemma, in div_le_lower_bound]
NZDivProp.div_small [lemma, in div_small]
NZDivProp.div_str_pos_iff [lemma, in div_str_pos_iff]
NZDivProp.div_str_pos [lemma, in div_str_pos]
NZDivProp.div_1_r [lemma, in div_1_r]
NZDivProp.div_lt_upper_bound [lemma, in div_lt_upper_bound]
NZDivProp.div_add_l [lemma, in div_add_l]
NZDivProp.mod_1_r [lemma, in mod_1_r]
NZDivProp.mod_small_iff [lemma, in mod_small_iff]
NZDivProp.mod_mul_r [lemma, in mod_mul_r]
NZDivProp.mod_unique [lemma, in mod_unique]
NZDivProp.mod_le [lemma, in mod_le]
NZDivProp.mod_add [lemma, in mod_add]
NZDivProp.mod_small [lemma, in mod_small]
NZDivProp.mod_mod [lemma, in mod_mod]
NZDivProp.mod_divides [lemma, in mod_divides]
NZDivProp.mod_0_l [lemma, in mod_0_l]
NZDivProp.mod_mul [lemma, in mod_mul]
NZDivProp.mod_same [lemma, in mod_same]
NZDivProp.mod_1_l [lemma, in mod_1_l]
NZDivProp.mul_succ_div_gt [lemma, in mul_succ_div_gt]
NZDivProp.mul_mod [lemma, in mul_mod]
NZDivProp.mul_mod_distr_r [lemma, in mul_mod_distr_r]
NZDivProp.mul_mod_distr_l [lemma, in mul_mod_distr_l]
NZDivProp.mul_mod_idemp_r [lemma, in mul_mod_idemp_r]
NZDivProp.mul_mod_idemp_l [lemma, in mul_mod_idemp_l]
NZDivProp.mul_div_le [lemma, in mul_div_le]
NZDivSpec [module, in NZDivSpec]
NZDivSpec.div_wd [instance, in div_wd]
NZDivSpec.div_mod [axiom, in div_mod]
NZDivSpec.mod_bound_pos [axiom, in mod_bound_pos]
NZDivSpec.mod_wd [instance, in mod_wd]
NZDiv' [module, in NZDiv']
NZDomain [library]
NZDomainProp [module, in NZDomainProp]
NZDomainProp.bi_induction_pred [lemma, in bi_induction_pred]
NZDomainProp.central_induction_pred [lemma, in central_induction_pred]
NZDomainProp.initial [definition, in initial]
NZDomainProp.InitialDontExists [section, in InitialDontExists]
NZDomainProp.InitialDontExists.succ_onto [variable, in succ_onto]
NZDomainProp.InitialExists [section, in InitialExists]
NZDomainProp.InitialExists.init [variable, in init]
NZDomainProp.InitialExists.Initial [variable, in Initial]
NZDomainProp.InitialExists.SuccPred [section, in SuccPred]
NZDomainProp.InitialExists.SuccPred.eq_decidable [variable, in eq_decidable]
NZDomainProp.initial_unique [lemma, in initial_unique]
NZDomainProp.initial_alt [lemma, in initial_alt]
NZDomainProp.initial_alt2 [lemma, in initial_alt2]
NZDomainProp.initial_ancestor [lemma, in initial_ancestor]
NZDomainProp.itersucc_or_iterpred [lemma, in itersucc_or_iterpred]
NZDomainProp.itersucc_or_itersucc [lemma, in itersucc_or_itersucc]
NZDomainProp.itersucc0_or_iterpred0 [lemma, in itersucc0_or_iterpred0]
NZDomainProp.succ_onto_gives_succ_pred [lemma, in succ_onto_gives_succ_pred]
NZDomainProp.succ_swap_pred [lemma, in succ_swap_pred]
NZDomainProp.succ_onto_pred_injective [lemma, in succ_onto_pred_injective]
NZDomainProp.succ_pred_approx [lemma, in succ_pred_approx]
NZDomainSig [module, in NZDomainSig]
NZDomainSig' [module, in NZDomainSig']
NZGcd [module, in NZGcd]
NZGcd [library]
NZGcdProp [module, in NZGcdProp]
NZGcdProp.divide_0_r [lemma, in divide_0_r]
NZGcdProp.divide_pos_le [lemma, in divide_pos_le]
NZGcdProp.divide_transitive [instance, in divide_transitive]
NZGcdProp.divide_factor_r [lemma, in divide_factor_r]
NZGcdProp.divide_refl [lemma, in divide_refl]
NZGcdProp.divide_factor_l [lemma, in divide_factor_l]
NZGcdProp.divide_gcd_iff [lemma, in divide_gcd_iff]
NZGcdProp.divide_1_r_nonneg [lemma, in divide_1_r_nonneg]
NZGcdProp.divide_mul_l [lemma, in divide_mul_l]
NZGcdProp.divide_antisym_nonneg [lemma, in divide_antisym_nonneg]
NZGcdProp.divide_reflexive [instance, in divide_reflexive]
NZGcdProp.divide_1_l [lemma, in divide_1_l]
NZGcdProp.divide_add_r [lemma, in divide_add_r]
NZGcdProp.divide_trans [lemma, in divide_trans]
NZGcdProp.divide_mul_r [lemma, in divide_mul_r]
NZGcdProp.divide_0_l [lemma, in divide_0_l]
NZGcdProp.divide_wd [instance, in divide_wd]
NZGcdProp.eq_mul_1_nonneg [lemma, in eq_mul_1_nonneg]
NZGcdProp.eq_mul_1_nonneg' [lemma, in eq_mul_1_nonneg']
NZGcdProp.gcd_diag_nonneg [lemma, in gcd_diag_nonneg]
NZGcdProp.gcd_0_l_nonneg [lemma, in gcd_0_l_nonneg]
NZGcdProp.gcd_0_r_nonneg [lemma, in gcd_0_r_nonneg]
NZGcdProp.gcd_comm [lemma, in gcd_comm]
NZGcdProp.gcd_eq_0_l [lemma, in gcd_eq_0_l]
NZGcdProp.gcd_wd [instance, in gcd_wd]
NZGcdProp.gcd_eq_0 [lemma, in gcd_eq_0]
NZGcdProp.gcd_eq_0_r [lemma, in gcd_eq_0_r]
NZGcdProp.gcd_divide_iff [lemma, in gcd_divide_iff]
NZGcdProp.gcd_1_r [lemma, in gcd_1_r]
NZGcdProp.gcd_unique_alt [lemma, in gcd_unique_alt]
NZGcdProp.gcd_unique [lemma, in gcd_unique]
NZGcdProp.gcd_assoc [lemma, in gcd_assoc]
NZGcdProp.gcd_mul_diag_l [lemma, in gcd_mul_diag_l]
NZGcdProp.gcd_1_l [lemma, in gcd_1_l]
NZGcdProp.mul_divide_mono_r [lemma, in mul_divide_mono_r]
NZGcdProp.mul_divide_mono_l [lemma, in mul_divide_mono_l]
NZGcdProp.mul_divide_cancel_r [lemma, in mul_divide_cancel_r]
NZGcdProp.mul_divide_cancel_l [lemma, in mul_divide_cancel_l]
NZGcdSpec [module, in NZGcdSpec]
NZGcdSpec.divide [definition, in divide]
NZGcdSpec.gcd_nonneg [axiom, in gcd_nonneg]
NZGcdSpec.gcd_greatest [axiom, in gcd_greatest]
NZGcdSpec.gcd_divide_r [axiom, in gcd_divide_r]
NZGcdSpec.gcd_divide_l [axiom, in gcd_divide_l]
( _ | _ ) [notation, in ::'('_x_'|'_x_')']
NZGcd' [module, in NZGcd']
NZLog [library]
NZLog2 [module, in NZLog2]
NZLog2Prop [module, in NZLog2Prop]
NZLog2Prop.add_log2_lt [lemma, in add_log2_lt]
NZLog2Prop.log2_le_mono [lemma, in log2_le_mono]
NZLog2Prop.log2_pos [lemma, in log2_pos]
NZLog2Prop.log2_wd [instance, in log2_wd]
NZLog2Prop.log2_eq_succ_iff_pow2 [lemma, in log2_eq_succ_iff_pow2]
NZLog2Prop.log2_succ_double [lemma, in log2_succ_double]
NZLog2Prop.log2_pow2 [lemma, in log2_pow2]
NZLog2Prop.log2_eq_succ_is_pow2 [lemma, in log2_eq_succ_is_pow2]
NZLog2Prop.log2_pred_pow2 [lemma, in log2_pred_pow2]
NZLog2Prop.log2_le_lin [lemma, in log2_le_lin]
NZLog2Prop.log2_le_pow2 [lemma, in log2_le_pow2]
NZLog2Prop.log2_succ_or [lemma, in log2_succ_or]
NZLog2Prop.log2_nonneg [lemma, in log2_nonneg]
NZLog2Prop.log2_mul_pow2 [lemma, in log2_mul_pow2]
NZLog2Prop.log2_lt_pow2 [lemma, in log2_lt_pow2]
NZLog2Prop.log2_mul_above [lemma, in log2_mul_above]
NZLog2Prop.log2_succ_le [lemma, in log2_succ_le]
NZLog2Prop.log2_unique' [lemma, in log2_unique']
NZLog2Prop.log2_lt_cancel [lemma, in log2_lt_cancel]
NZLog2Prop.log2_same [lemma, in log2_same]
NZLog2Prop.log2_double [lemma, in log2_double]
NZLog2Prop.log2_null [lemma, in log2_null]
NZLog2Prop.log2_lt_lin [lemma, in log2_lt_lin]
NZLog2Prop.log2_mul_below [lemma, in log2_mul_below]
NZLog2Prop.log2_1 [lemma, in log2_1]
NZLog2Prop.log2_2 [lemma, in log2_2]
NZLog2Prop.log2_add_le [lemma, in log2_add_le]
NZLog2Prop.log2_unique [lemma, in log2_unique]
NZLog2Prop.log2_spec_alt [lemma, in log2_spec_alt]
NZLog2Spec [module, in NZLog2Spec]
NZLog2Spec.log2_spec [axiom, in log2_spec]
NZLog2Spec.log2_nonpos [axiom, in log2_nonpos]
NZLog2UpProp [module, in NZLog2UpProp]
NZLog2UpProp.add_log2_up_lt [lemma, in add_log2_up_lt]
NZLog2UpProp.le_log2_log2_up [lemma, in le_log2_log2_up]
NZLog2UpProp.le_log2_up_succ_log2 [lemma, in le_log2_up_succ_log2]
NZLog2UpProp.log2_up_null [lemma, in log2_up_null]
NZLog2UpProp.log2_up_succ_pow2 [lemma, in log2_up_succ_pow2]
NZLog2UpProp.log2_up_double [lemma, in log2_up_double]
NZLog2UpProp.log2_up_le_mono [lemma, in log2_up_le_mono]
NZLog2UpProp.log2_up_mul_pow2 [lemma, in log2_up_mul_pow2]
NZLog2UpProp.log2_up_wd [instance, in log2_up_wd]
NZLog2UpProp.log2_up_le_pow2 [lemma, in log2_up_le_pow2]
NZLog2UpProp.log2_log2_up_exact [lemma, in log2_log2_up_exact]
NZLog2UpProp.log2_up_same [lemma, in log2_up_same]
NZLog2UpProp.log2_up_succ_or [lemma, in log2_up_succ_or]
NZLog2UpProp.log2_up_lt_cancel [lemma, in log2_up_lt_cancel]
NZLog2UpProp.log2_up_pos [lemma, in log2_up_pos]
NZLog2UpProp.log2_up_mul_above [lemma, in log2_up_mul_above]
NZLog2UpProp.log2_up_lt_pow2 [lemma, in log2_up_lt_pow2]
NZLog2UpProp.log2_up_pow2 [lemma, in log2_up_pow2]
NZLog2UpProp.log2_up_eqn [lemma, in log2_up_eqn]
NZLog2UpProp.log2_up_1 [lemma, in log2_up_1]
NZLog2UpProp.log2_log2_up_spec [lemma, in log2_log2_up_spec]
NZLog2UpProp.log2_up_succ_double [lemma, in log2_up_succ_double]
NZLog2UpProp.log2_up_eq_succ_iff_pow2 [lemma, in log2_up_eq_succ_iff_pow2]
NZLog2UpProp.log2_up_nonneg [lemma, in log2_up_nonneg]
NZLog2UpProp.log2_up [definition, in log2_up]
NZLog2UpProp.log2_up_2 [lemma, in log2_up_2]
NZLog2UpProp.log2_up_spec [lemma, in log2_up_spec]
NZLog2UpProp.log2_up_unique [lemma, in log2_up_unique]
NZLog2UpProp.log2_up_add_le [lemma, in log2_up_add_le]
NZLog2UpProp.log2_up_mul_below [lemma, in log2_up_mul_below]
NZLog2UpProp.log2_up_le_lin [lemma, in log2_up_le_lin]
NZLog2UpProp.log2_up_succ_le [lemma, in log2_up_succ_le]
NZLog2UpProp.log2_up_nonpos [lemma, in log2_up_nonpos]
NZLog2UpProp.log2_up_eq_succ_is_pow2 [lemma, in log2_up_eq_succ_is_pow2]
NZLog2UpProp.log2_up_lt_lin [lemma, in log2_up_lt_lin]
NZLog2UpProp.log2_up_eqn0 [lemma, in log2_up_eqn0]
NZMul [library]
NZMulOrder [library]
NZMulOrderProp [module, in NZMulOrderProp]
NZMulOrderProp.add_square_le [lemma, in add_square_le]
NZMulOrderProp.add_le_mul [lemma, in add_le_mul]
NZMulOrderProp.crossmul_le_addsquare [lemma, in crossmul_le_addsquare]
NZMulOrderProp.eq_mul_0_r [lemma, in eq_mul_0_r]
NZMulOrderProp.eq_mul_0 [lemma, in eq_mul_0]
NZMulOrderProp.eq_mul_0_l [lemma, in eq_mul_0_l]
NZMulOrderProp.eq_square_0 [lemma, in eq_square_0]
NZMulOrderProp.lt_0_mul [lemma, in lt_0_mul]
NZMulOrderProp.lt_1_mul_pos [lemma, in lt_1_mul_pos]
NZMulOrderProp.mul_le_mono_nonpos_l [lemma, in mul_le_mono_nonpos_l]
NZMulOrderProp.mul_le_mono_pos_r [lemma, in mul_le_mono_pos_r]
NZMulOrderProp.mul_le_mono_neg_l [lemma, in mul_le_mono_neg_l]
NZMulOrderProp.mul_le_mono_pos_l [lemma, in mul_le_mono_pos_l]
NZMulOrderProp.mul_lt_mono_neg_r [lemma, in mul_lt_mono_neg_r]
NZMulOrderProp.mul_eq_0_r [definition, in mul_eq_0_r]
NZMulOrderProp.mul_le_mono_nonneg_r [lemma, in mul_le_mono_nonneg_r]
NZMulOrderProp.mul_lt_mono_nonneg [lemma, in mul_lt_mono_nonneg]
NZMulOrderProp.mul_lt_pred [lemma, in mul_lt_pred]
NZMulOrderProp.mul_lt_mono_pos_r [lemma, in mul_lt_mono_pos_r]
NZMulOrderProp.mul_pos_cancel_l [lemma, in mul_pos_cancel_l]
NZMulOrderProp.mul_eq_0_l [definition, in mul_eq_0_l]
NZMulOrderProp.mul_pos_pos [lemma, in mul_pos_pos]
NZMulOrderProp.mul_2_mono_l [lemma, in mul_2_mono_l]
NZMulOrderProp.mul_cancel_l [lemma, in mul_cancel_l]
NZMulOrderProp.mul_cancel_r [lemma, in mul_cancel_r]
NZMulOrderProp.mul_le_mono_neg_r [lemma, in mul_le_mono_neg_r]
NZMulOrderProp.mul_lt_mono_neg_l [lemma, in mul_lt_mono_neg_l]
NZMulOrderProp.mul_le_mono_nonneg_l [lemma, in mul_le_mono_nonneg_l]
NZMulOrderProp.mul_le_mono_nonneg [lemma, in mul_le_mono_nonneg]
NZMulOrderProp.mul_le_mono_nonpos_r [lemma, in mul_le_mono_nonpos_r]
NZMulOrderProp.mul_lt_mono_pos_l [lemma, in mul_lt_mono_pos_l]
NZMulOrderProp.mul_eq_0 [definition, in mul_eq_0]
NZMulOrderProp.mul_pos_cancel_r [lemma, in mul_pos_cancel_r]
NZMulOrderProp.mul_neg_neg [lemma, in mul_neg_neg]
NZMulOrderProp.mul_pos_neg [lemma, in mul_pos_neg]
NZMulOrderProp.mul_nonneg_nonneg [lemma, in mul_nonneg_nonneg]
NZMulOrderProp.mul_neg_pos [lemma, in mul_neg_pos]
NZMulOrderProp.mul_id_r [lemma, in mul_id_r]
NZMulOrderProp.mul_id_l [lemma, in mul_id_l]
NZMulOrderProp.mul_nonneg_cancel_l [lemma, in mul_nonneg_cancel_l]
NZMulOrderProp.mul_nonneg_cancel_r [lemma, in mul_nonneg_cancel_r]
NZMulOrderProp.neq_mul_0 [lemma, in neq_mul_0]
NZMulOrderProp.quadmul_le_squareadd [lemma, in quadmul_le_squareadd]
NZMulOrderProp.square_le_simpl_nonneg [lemma, in square_le_simpl_nonneg]
NZMulOrderProp.square_lt_mono_nonneg [lemma, in square_lt_mono_nonneg]
NZMulOrderProp.square_lt_simpl_nonneg [lemma, in square_lt_simpl_nonneg]
NZMulOrderProp.square_le_mono_nonneg [lemma, in square_le_mono_nonneg]
NZMulOrderProp.square_nonneg [lemma, in square_nonneg]
NZMulOrderProp.square_add_le [lemma, in square_add_le]
NZMulProp [module, in NZMulProp]
NZMulProp.mul_shuffle1 [lemma, in mul_shuffle1]
NZMulProp.mul_shuffle3 [lemma, in mul_shuffle3]
NZMulProp.mul_1_r [lemma, in mul_1_r]
NZMulProp.mul_add_distr_l [lemma, in mul_add_distr_l]
NZMulProp.mul_1_l [lemma, in mul_1_l]
NZMulProp.mul_succ_r [lemma, in mul_succ_r]
NZMulProp.mul_add_distr_r [lemma, in mul_add_distr_r]
NZMulProp.mul_shuffle2 [lemma, in mul_shuffle2]
NZMulProp.mul_0_r [lemma, in mul_0_r]
NZMulProp.mul_comm [lemma, in mul_comm]
NZMulProp.mul_assoc [lemma, in mul_assoc]
NZMulProp.mul_shuffle0 [lemma, in mul_shuffle0]
NZOfNat [module, in NZOfNat]
NZOfNatOps [module, in NZOfNatOps]
NZOfNatOps.ofnat_sub_r [lemma, in ofnat_sub_r]
NZOfNatOps.ofnat_sub [lemma, in ofnat_sub]
NZOfNatOps.ofnat_mul [lemma, in ofnat_mul]
NZOfNatOps.ofnat_add [lemma, in ofnat_add]
NZOfNatOps.ofnat_add_l [lemma, in ofnat_add_l]
NZOfNatOrd [module, in NZOfNatOrd]
NZOfNatOrd.ofnat_eq [lemma, in ofnat_eq]
NZOfNatOrd.ofnat_S_neq_0 [lemma, in ofnat_S_neq_0]
NZOfNatOrd.ofnat_lt [lemma, in ofnat_lt]
NZOfNatOrd.ofnat_le [lemma, in ofnat_le]
NZOfNatOrd.ofnat_injective [lemma, in ofnat_injective]
NZOfNatOrd.ofnat_S_gt_0 [lemma, in ofnat_S_gt_0]
NZOfNat.ofnat [definition, in ofnat]
NZOfNat.ofnat_succ [lemma, in ofnat_succ]
NZOfNat.ofnat_zero [lemma, in ofnat_zero]
NZOfNat.ofnat_pred [lemma, in ofnat_pred]
[ _ ] (ofnat) [notation, in :ofnat:'['_x_']']
NZOrd [module, in NZOrd]
NZOrdAxiomsSig [module, in NZOrdAxiomsSig]
NZOrdAxiomsSig' [module, in NZOrdAxiomsSig']
NZOrder [library]
NZOrderedType [module, in NZOrderedType]
NZOrderProp [module, in NZOrderProp]
NZOrderProp.A'A_right [lemma, in A'A_right]
NZOrderProp.A'A_left [lemma, in A'A_left]
NZOrderProp.eq_dne [lemma, in eq_dne]
NZOrderProp.eq_decidable [lemma, in eq_decidable]
NZOrderProp.eq_le_incl [lemma, in eq_le_incl]
NZOrderProp.gt_wf [lemma, in gt_wf]
NZOrderProp.Induction [section, in Induction]
NZOrderProp.Induction.A [variable, in A]
NZOrderProp.Induction.A_wd [variable, in A_wd]
NZOrderProp.Induction.Center [section, in Center]
NZOrderProp.Induction.Center.LeftInduction [section, in LeftInduction]
NZOrderProp.Induction.Center.LeftInduction.A' [variable, in A']
NZOrderProp.Induction.Center.LeftInduction.left_step' [variable, in left_step']
NZOrderProp.Induction.Center.LeftInduction.left_step [variable, in left_step]
NZOrderProp.Induction.Center.LeftInduction.left_step'' [variable, in left_step'']
NZOrderProp.Induction.Center.RightInduction [section, in RightInduction]
NZOrderProp.Induction.Center.RightInduction.A' [variable, in A']
NZOrderProp.Induction.Center.RightInduction.right_step [variable, in right_step]
NZOrderProp.Induction.Center.RightInduction.right_step' [variable, in right_step']
NZOrderProp.Induction.Center.RightInduction.right_step'' [variable, in right_step'']
NZOrderProp.Induction.Center.z [variable, in z]
NZOrderProp.lbase [lemma, in lbase]
NZOrderProp.left_induction' [lemma, in left_induction']
NZOrderProp.left_induction [lemma, in left_induction]
NZOrderProp.le_lteq [definition, in le_lteq]
NZOrderProp.le_stepr [lemma, in le_stepr]
NZOrderProp.le_wd [instance, in le_wd]
NZOrderProp.le_ind [lemma, in le_ind]
NZOrderProp.le_trans [lemma, in le_trans]
NZOrderProp.le_ngt [lemma, in le_ngt]
NZOrderProp.le_dne [lemma, in le_dne]
NZOrderProp.le_preorder [instance, in le_preorder]
NZOrderProp.le_partialorder [instance, in le_partialorder]
NZOrderProp.le_neq [lemma, in le_neq]
NZOrderProp.le_succ_diag_r [lemma, in le_succ_diag_r]
NZOrderProp.le_succ_r [lemma, in le_succ_r]
NZOrderProp.le_gt_cases [lemma, in le_gt_cases]
NZOrderProp.le_decidable [lemma, in le_decidable]
NZOrderProp.le_0_2 [lemma, in le_0_2]
NZOrderProp.le_stepl [lemma, in le_stepl]
NZOrderProp.le_antisymm [lemma, in le_antisymm]
NZOrderProp.le_0_1 [lemma, in le_0_1]
NZOrderProp.le_le_succ_r [lemma, in le_le_succ_r]
NZOrderProp.le_succ_l [lemma, in le_succ_l]
NZOrderProp.le_lt_trans [lemma, in le_lt_trans]
NZOrderProp.le_refl [lemma, in le_refl]
NZOrderProp.le_ge_cases [lemma, in le_ge_cases]
NZOrderProp.ls_ls' [lemma, in ls_ls']
NZOrderProp.ls'_ls'' [lemma, in ls'_ls'']
NZOrderProp.lt_lt_succ_r [lemma, in lt_lt_succ_r]
NZOrderProp.lt_asymm [lemma, in lt_asymm]
NZOrderProp.lt_le_incl [lemma, in lt_le_incl]
NZOrderProp.lt_exists_pred_strong [lemma, in lt_exists_pred_strong]
NZOrderProp.lt_gt_cases [lemma, in lt_gt_cases]
NZOrderProp.lt_compat [definition, in lt_compat]
NZOrderProp.lt_strorder [instance, in lt_strorder]
NZOrderProp.lt_stepr [lemma, in lt_stepr]
NZOrderProp.lt_ind [lemma, in lt_ind]
NZOrderProp.lt_stepl [lemma, in lt_stepl]
NZOrderProp.lt_succ_l [lemma, in lt_succ_l]
NZOrderProp.lt_nge [lemma, in lt_nge]
NZOrderProp.lt_0_2 [lemma, in lt_0_2]
NZOrderProp.lt_le_trans [lemma, in lt_le_trans]
NZOrderProp.lt_exists_pred [lemma, in lt_exists_pred]
NZOrderProp.lt_wf [lemma, in lt_wf]
NZOrderProp.lt_dne [lemma, in lt_dne]
NZOrderProp.lt_0_1 [lemma, in lt_0_1]
NZOrderProp.lt_succ_pred [lemma, in lt_succ_pred]
NZOrderProp.lt_total [definition, in lt_total]
NZOrderProp.lt_decidable [lemma, in lt_decidable]
NZOrderProp.lt_1_2 [lemma, in lt_1_2]
NZOrderProp.lt_trans [lemma, in lt_trans]
NZOrderProp.lt_succ_diag_r [lemma, in lt_succ_diag_r]
NZOrderProp.lt_1_l [lemma, in lt_1_l]
NZOrderProp.lt_neq [lemma, in lt_neq]
NZOrderProp.lt_ngt [abbreviation, in lt_ngt]
NZOrderProp.lt_eq_gt_cases [abbreviation, in lt_eq_gt_cases]
NZOrderProp.lt_ge_cases [lemma, in lt_ge_cases]
NZOrderProp.lt_trichotomy [lemma, in lt_trichotomy]
NZOrderProp.neq_succ_diag_r [lemma, in neq_succ_diag_r]
NZOrderProp.neq_succ_diag_l [lemma, in neq_succ_diag_l]
NZOrderProp.nle_gt [lemma, in nle_gt]
NZOrderProp.nle_succ_diag_l [lemma, in nle_succ_diag_l]
NZOrderProp.nlt_ge [lemma, in nlt_ge]
NZOrderProp.nlt_succ_r [lemma, in nlt_succ_r]
NZOrderProp.nlt_succ_diag_l [lemma, in nlt_succ_diag_l]
NZOrderProp.order_induction' [lemma, in order_induction']
NZOrderProp.order_induction [lemma, in order_induction]
NZOrderProp.order_induction'_0 [lemma, in order_induction'_0]
NZOrderProp.order_induction_0 [lemma, in order_induction_0]
NZOrderProp.Private_OrderTac.Elts.le_lteq [definition, in le_lteq]
NZOrderProp.Private_OrderTac.Tac [module, in NZOrderProp.Private_OrderTac.Tac]
NZOrderProp.Private_OrderTac.Elts.lt_compat [definition, in lt_compat]
NZOrderProp.Private_OrderTac.Elts.lt_strorder [definition, in lt_strorder]
NZOrderProp.Private_OrderTac.Elts.t [definition, in t]
NZOrderProp.Private_OrderTac.Elts.le [definition, in le]
NZOrderProp.Private_OrderTac.Elts.lt_total [definition, in lt_total]
NZOrderProp.Private_OrderTac.Elts [module, in NZOrderProp.Private_OrderTac.Elts]
NZOrderProp.Private_OrderTac [module, in NZOrderProp.Private_OrderTac]
NZOrderProp.Private_OrderTac.Elts.eq_equiv [definition, in eq_equiv]
NZOrderProp.Private_OrderTac.Elts.lt [definition, in lt]
NZOrderProp.Private_OrderTac.Elts.eq [definition, in eq]
NZOrderProp.rbase [lemma, in rbase]
NZOrderProp.Rgt_wd [instance, in Rgt_wd]
NZOrderProp.right_induction' [lemma, in right_induction']
NZOrderProp.right_induction [lemma, in right_induction]
NZOrderProp.Rlt_wd [instance, in Rlt_wd]
NZOrderProp.rs_rs' [lemma, in rs_rs']
NZOrderProp.rs'_rs'' [lemma, in rs'_rs'']
NZOrderProp.strong_right_induction [lemma, in strong_right_induction]
NZOrderProp.strong_left_induction' [lemma, in strong_left_induction']
NZOrderProp.strong_left_induction [lemma, in strong_left_induction]
NZOrderProp.strong_right_induction' [lemma, in strong_right_induction']
NZOrderProp.succ_lt_mono [lemma, in succ_lt_mono]
NZOrderProp.succ_le_mono [lemma, in succ_le_mono]
NZOrderProp.WF [section, in WF]
NZOrderProp.WF.Rgt [variable, in Rgt]
NZOrderProp.WF.Rlt [variable, in Rlt]
NZOrderProp.WF.z [variable, in z]
NZOrdSig [module, in NZOrdSig]
NZOrdSig' [module, in NZOrdSig']
NZOrd' [module, in NZOrd']
Nzorn [lemma, in Nzorn]
NZParity [module, in NZParity]
NZParity [library]
NZParityProp [module, in NZParityProp]
NZParityProp.double_above [lemma, in double_above]
NZParityProp.double_below [lemma, in double_below]
NZParityProp.even_0 [lemma, in even_0]
NZParityProp.Even_Odd_False [lemma, in Even_Odd_False]
NZParityProp.even_add [lemma, in even_add]
NZParityProp.even_mul [lemma, in even_mul]
NZParityProp.Even_wd [instance, in Even_wd]
NZParityProp.even_succ_succ [lemma, in even_succ_succ]
NZParityProp.even_wd [instance, in even_wd]
NZParityProp.even_2 [lemma, in even_2]
NZParityProp.even_add_mul_2 [lemma, in even_add_mul_2]
NZParityProp.even_add_even [lemma, in even_add_even]
NZParityProp.even_1 [lemma, in even_1]
NZParityProp.Even_succ_succ [lemma, in Even_succ_succ]
NZParityProp.Even_or_Odd [lemma, in Even_or_Odd]
NZParityProp.even_succ [lemma, in even_succ]
NZParityProp.even_add_mul_even [lemma, in even_add_mul_even]
NZParityProp.Even_succ [lemma, in Even_succ]
NZParityProp.negb_odd [lemma, in negb_odd]
NZParityProp.negb_even [lemma, in negb_even]
NZParityProp.odd_mul [lemma, in odd_mul]
NZParityProp.odd_add_mul_2 [lemma, in odd_add_mul_2]
NZParityProp.odd_add_even [lemma, in odd_add_even]
NZParityProp.odd_2 [lemma, in odd_2]
NZParityProp.odd_succ [lemma, in odd_succ]
NZParityProp.odd_wd [instance, in odd_wd]
NZParityProp.odd_add [lemma, in odd_add]
NZParityProp.Odd_succ [lemma, in Odd_succ]
NZParityProp.Odd_succ_succ [lemma, in Odd_succ_succ]
NZParityProp.Odd_wd [instance, in Odd_wd]
NZParityProp.odd_1 [lemma, in odd_1]
NZParityProp.odd_succ_succ [lemma, in odd_succ_succ]
NZParityProp.odd_0 [lemma, in odd_0]
NZParityProp.odd_add_mul_even [lemma, in odd_add_mul_even]
NZParityProp.orb_even_odd [lemma, in orb_even_odd]
NZParity.Even [definition, in Even]
NZParity.even [axiom, in even]
NZParity.even_spec [axiom, in even_spec]
NZParity.odd [axiom, in odd]
NZParity.Odd [definition, in Odd]
NZParity.odd_spec [axiom, in odd_spec]
NZPow [module, in NZPow]
NZPow [library]
NZPowProp [module, in NZPowProp]
NZPowProp.pow_0_l' [lemma, in pow_0_l']
NZPowProp.pow_le_mono_r [lemma, in pow_le_mono_r]
NZPowProp.pow_inj_l [lemma, in pow_inj_l]
NZPowProp.pow_nonneg [lemma, in pow_nonneg]
NZPowProp.pow_lt_mono [lemma, in pow_lt_mono]
NZPowProp.pow_le_mono_l_iff [lemma, in pow_le_mono_l_iff]
NZPowProp.pow_nonzero [lemma, in pow_nonzero]
NZPowProp.pow_lt_mono_l [lemma, in pow_lt_mono_l]
NZPowProp.pow_le_mono_r_iff [lemma, in pow_le_mono_r_iff]
NZPowProp.pow_le_mono_l [lemma, in pow_le_mono_l]
NZPowProp.pow_gt_lin_r [lemma, in pow_gt_lin_r]
NZPowProp.pow_1_l [lemma, in pow_1_l]
NZPowProp.pow_0_l [lemma, in pow_0_l]
NZPowProp.pow_mul_r [lemma, in pow_mul_r]
NZPowProp.pow_add_r [lemma, in pow_add_r]
NZPowProp.pow_1_r [lemma, in pow_1_r]
NZPowProp.pow_lt_mono_r_iff [lemma, in pow_lt_mono_r_iff]
NZPowProp.pow_2_r [lemma, in pow_2_r]
NZPowProp.pow_lt_mono_l_iff [lemma, in pow_lt_mono_l_iff]
NZPowProp.pow_eq_0_iff [lemma, in pow_eq_0_iff]
NZPowProp.pow_add_upper [lemma, in pow_add_upper]
NZPowProp.pow_le_mono [lemma, in pow_le_mono]
NZPowProp.pow_eq_0 [lemma, in pow_eq_0]
NZPowProp.pow_pos_nonneg [lemma, in pow_pos_nonneg]
NZPowProp.pow_add_lower [lemma, in pow_add_lower]
NZPowProp.pow_gt_1 [lemma, in pow_gt_1]
NZPowProp.pow_mul_l [lemma, in pow_mul_l]
NZPowProp.pow_inj_r [lemma, in pow_inj_r]
NZPowProp.pow_lt_mono_r [lemma, in pow_lt_mono_r]
NZPowSpec [module, in NZPowSpec]
NZPowSpec.pow_wd [instance, in pow_wd]
NZPowSpec.pow_0_r [axiom, in pow_0_r]
NZPowSpec.pow_succ_r [axiom, in pow_succ_r]
NZPowSpec.pow_neg_r [axiom, in pow_neg_r]
NZPow' [module, in NZPow']
NZProp [module, in NZProp]
NZProperties [library]
NZSqrt [module, in NZSqrt]
NZSqrt [library]
NZSqrtProp [module, in NZSqrtProp]
NZSqrtProp.add_sqrt_le [lemma, in add_sqrt_le]
NZSqrtProp.sqrt_unique [lemma, in sqrt_unique]
NZSqrtProp.sqrt_le_mono [lemma, in sqrt_le_mono]
NZSqrtProp.sqrt_mul_below [lemma, in sqrt_mul_below]
NZSqrtProp.sqrt_le_lin [lemma, in sqrt_le_lin]
NZSqrtProp.sqrt_1 [lemma, in sqrt_1]
NZSqrtProp.sqrt_0 [lemma, in sqrt_0]
NZSqrtProp.sqrt_lt_cancel [lemma, in sqrt_lt_cancel]
NZSqrtProp.sqrt_succ_le [lemma, in sqrt_succ_le]
NZSqrtProp.sqrt_eq_succ_iff_square [lemma, in sqrt_eq_succ_iff_square]
NZSqrtProp.sqrt_le_square [lemma, in sqrt_le_square]
NZSqrtProp.sqrt_spec_alt [lemma, in sqrt_spec_alt]
NZSqrtProp.sqrt_unique' [lemma, in sqrt_unique']
NZSqrtProp.sqrt_succ_or [lemma, in sqrt_succ_or]
NZSqrtProp.sqrt_add_le [lemma, in sqrt_add_le]
NZSqrtProp.sqrt_2 [lemma, in sqrt_2]
NZSqrtProp.sqrt_nonneg [lemma, in sqrt_nonneg]
NZSqrtProp.sqrt_wd [instance, in sqrt_wd]
NZSqrtProp.sqrt_lt_square [lemma, in sqrt_lt_square]
NZSqrtProp.sqrt_lt_lin [lemma, in sqrt_lt_lin]
NZSqrtProp.sqrt_spec_nonneg [lemma, in sqrt_spec_nonneg]
NZSqrtProp.sqrt_mul_above [lemma, in sqrt_mul_above]
NZSqrtProp.sqrt_square [lemma, in sqrt_square]
NZSqrtProp.sqrt_pos [lemma, in sqrt_pos]
NZSqrtProp.sqrt_pred_square [lemma, in sqrt_pred_square]
_ ² [notation, in ::x_'²']
NZSqrtSpec [module, in NZSqrtSpec]
NZSqrtSpec.sqrt_spec [axiom, in sqrt_spec]
NZSqrtSpec.sqrt_neg [axiom, in sqrt_neg]
NZSqrtUpProp [module, in NZSqrtUpProp]
NZSqrtUpProp.add_sqrt_up_le [lemma, in add_sqrt_up_le]
NZSqrtUpProp.le_sqrt_sqrt_up [lemma, in le_sqrt_sqrt_up]
NZSqrtUpProp.le_sqrt_up_succ_sqrt [lemma, in le_sqrt_up_succ_sqrt]
NZSqrtUpProp.sqrt_up [definition, in sqrt_up]
NZSqrtUpProp.sqrt_up_mul_above [lemma, in sqrt_up_mul_above]
NZSqrtUpProp.sqrt_up_spec [lemma, in sqrt_up_spec]
NZSqrtUpProp.sqrt_up_1 [lemma, in sqrt_up_1]
NZSqrtUpProp.sqrt_up_le_square [lemma, in sqrt_up_le_square]
NZSqrtUpProp.sqrt_up_nonneg [lemma, in sqrt_up_nonneg]
NZSqrtUpProp.sqrt_up_eqn [lemma, in sqrt_up_eqn]
NZSqrtUpProp.sqrt_up_0 [lemma, in sqrt_up_0]
NZSqrtUpProp.sqrt_up_mul_below [lemma, in sqrt_up_mul_below]
NZSqrtUpProp.sqrt_up_eqn0 [lemma, in sqrt_up_eqn0]
NZSqrtUpProp.sqrt_sqrt_up_spec [lemma, in sqrt_sqrt_up_spec]
NZSqrtUpProp.sqrt_up_unique [lemma, in sqrt_up_unique]
NZSqrtUpProp.sqrt_up_lt_square [lemma, in sqrt_up_lt_square]
NZSqrtUpProp.sqrt_up_succ_or [lemma, in sqrt_up_succ_or]
NZSqrtUpProp.sqrt_up_succ_le [lemma, in sqrt_up_succ_le]
NZSqrtUpProp.sqrt_up_2 [lemma, in sqrt_up_2]
NZSqrtUpProp.sqrt_up_wd [instance, in sqrt_up_wd]
NZSqrtUpProp.sqrt_up_add_le [lemma, in sqrt_up_add_le]
NZSqrtUpProp.sqrt_up_eq_succ_iff_square [lemma, in sqrt_up_eq_succ_iff_square]
NZSqrtUpProp.sqrt_sqrt_up_exact [lemma, in sqrt_sqrt_up_exact]
NZSqrtUpProp.sqrt_up_pos [lemma, in sqrt_up_pos]
NZSqrtUpProp.sqrt_up_succ_square [lemma, in sqrt_up_succ_square]
NZSqrtUpProp.sqrt_up_lt_cancel [lemma, in sqrt_up_lt_cancel]
NZSqrtUpProp.sqrt_up_le_lin [lemma, in sqrt_up_le_lin]
NZSqrtUpProp.sqrt_up_le_mono [lemma, in sqrt_up_le_mono]
NZSqrtUpProp.sqrt_up_square [lemma, in sqrt_up_square]
NZSqrtUpProp.sqrt_up_lt_lin [lemma, in sqrt_up_lt_lin]
_ ² [notation, in ::x_'²']
√° _ [notation, in ::'√°'_x]
NZSqrt' [module, in NZSqrt']
NZSquare [module, in NZSquare]
NZSquare.square [axiom, in square]
NZSquare.square_spec [axiom, in square_spec]
N_ind_double [definition, in N_ind_double]
N_as_OT.eq_refl [definition, in eq_refl]
N_of_nat_of_N [abbreviation, in N_of_nat_of_N]
N_of_div2 [abbreviation, in N_of_div2]
N_of_pred [abbreviation, in N_of_pred]
N_of_ascii [definition, in N_of_ascii]
N_ind [abbreviation, in N_ind]
N_rect [abbreviation, in N_rect]
N_nat_Z [lemma, in N_nat_Z]
N_of_nat_compare [abbreviation, in N_of_nat_compare]
N_of_minus [abbreviation, in N_of_minus]
N_of_min [abbreviation, in N_of_min]
n_SSSn [lemma, in n_SSSn]
N_as_DT [module, in N_as_DT]
N_as_DT [module, in N_as_DT]
n_SSn [lemma, in n_SSn]
N_of_plus [abbreviation, in N_of_plus]
N_as_OT.t [definition, in t]
N_eq_dec [abbreviation, in N_eq_dec]
N_digits [definition, in N_digits]
N_as_OT.compare [definition, in compare]
N_of_double [abbreviation, in N_of_double]
n_SSSSn [lemma, in n_SSSSn]
N_of_nat [abbreviation, in N_of_nat]
N_of_digits [definition, in N_of_digits]
N_of_max [abbreviation, in N_of_max]
N_as_OT.eq_sym [definition, in eq_sym]
N_ascii_embedding [lemma, in N_ascii_embedding]
N_as_OT.lt_not_eq [definition, in lt_not_eq]
N_of_mult [abbreviation, in N_of_mult]
N_as_OT [module, in N_as_OT]
N_as_OT [module, in N_as_OT]
N_as_OT.lt_trans [definition, in lt_trans]
N_as_OT.eq_trans [definition, in eq_trans]
N_of_S [abbreviation, in N_of_S]
N_as_OT.eq_dec [definition, in eq_dec]
N_of_double_plus_one [abbreviation, in N_of_double_plus_one]
N_of_nat_inj [abbreviation, in N_of_nat_inj]
N_rec [abbreviation, in N_rec]
N_as_OT.lt [definition, in lt]
N_rec_double [definition, in N_rec_double]
n_Sn [lemma, in n_Sn]
N_as_OT.eq [definition, in eq]
N.add [definition, in add]
N.add_succ_l [lemma, in add_succ_l]
N.add_0_l [lemma, in add_0_l]
N.add_wd [definition, in add_wd]
N.binary_ind [definition, in binary_ind]
N.binary_rec [definition, in binary_rec]
N.binary_rect [definition, in binary_rect]
N.bi_induction [lemma, in bi_induction]
N.compare [definition, in compare]
N.compare_lt_iff [lemma, in compare_lt_iff]
N.compare_antisym [lemma, in compare_antisym]
N.compare_0_r [lemma, in compare_0_r]
N.compare_le_iff [lemma, in compare_le_iff]
N.compare_eq_iff [lemma, in compare_eq_iff]
N.discr [definition, in discr]
N.div [definition, in div]
N.divide [definition, in divide]
N.div_eucl [definition, in div_eucl]
N.div_mod' [lemma, in div_mod']
N.div_eucl_spec [lemma, in div_eucl_spec]
N.div_wd [definition, in div_wd]
N.div_mod [definition, in div_mod]
N.div2 [definition, in div2]
N.div2_double [lemma, in div2_double]
N.div2_spec [definition, in div2_spec]
N.div2_succ_double [lemma, in div2_succ_double]
N.double [definition, in double]
N.double_add [lemma, in double_add]
N.double_mul [lemma, in double_mul]
N.double_spec [lemma, in double_spec]
N.double_inj [lemma, in double_inj]
N.eq [definition, in eq]
N.eqb [definition, in eqb]
N.eqb_eq [lemma, in eqb_eq]
N.eq_dec [definition, in eq_dec]
N.eq_equiv [definition, in eq_equiv]
N.Even [definition, in Even]
N.even [definition, in even]
N.even_spec [lemma, in even_spec]
N.gcd [definition, in gcd]
N.gcd_nonneg [lemma, in gcd_nonneg]
N.gcd_greatest [lemma, in gcd_greatest]
N.gcd_divide_r [lemma, in gcd_divide_r]
N.gcd_divide_l [lemma, in gcd_divide_l]
N.ge [definition, in ge]
N.ge_le [lemma, in ge_le]
N.ge_le_iff [lemma, in ge_le_iff]
N.ggcd [definition, in ggcd]
N.ggcd_correct_divisors [lemma, in ggcd_correct_divisors]
N.ggcd_gcd [lemma, in ggcd_gcd]
N.gt [definition, in gt]
N.gt_lt [lemma, in gt_lt]
N.gt_lt_iff [lemma, in gt_lt_iff]
N.iter [definition, in iter]
N.land [definition, in land]
N.land_spec [lemma, in land_spec]
N.ldiff [definition, in ldiff]
N.ldiff_spec [lemma, in ldiff_spec]
N.le [definition, in le]
N.leb [definition, in leb]
N.leb_le [lemma, in leb_le]
N.le_ge [lemma, in le_ge]
N.log2 [definition, in log2]
N.log2_spec [lemma, in log2_spec]
N.log2_nonpos [lemma, in log2_nonpos]
N.lor [definition, in lor]
N.lor_spec [lemma, in lor_spec]
N.lt [definition, in lt]
N.ltb [definition, in ltb]
N.ltb_lt [lemma, in ltb_lt]
N.lt_succ_r [lemma, in lt_succ_r]
N.lt_gt [lemma, in lt_gt]
N.lt_wd [definition, in lt_wd]
N.lxor [definition, in lxor]
N.lxor_spec [lemma, in lxor_spec]
N.max [definition, in max]
N.max_r [lemma, in max_r]
N.max_l [lemma, in max_l]
N.min [definition, in min]
N.min_r [lemma, in min_r]
N.min_l [lemma, in min_l]
N.modulo [definition, in modulo]
N.mod_bound_pos [lemma, in mod_bound_pos]
N.mod_lt [lemma, in mod_lt]
N.mod_wd [definition, in mod_wd]
N.mul [definition, in mul]
N.mul_succ_l [lemma, in mul_succ_l]
N.mul_0_l [lemma, in mul_0_l]
N.mul_wd [definition, in mul_wd]
N.odd [definition, in odd]
N.Odd [definition, in Odd]
N.odd_spec [lemma, in odd_spec]
N.of_nat [definition, in of_nat]
N.one [definition, in one]
N.one_succ [lemma, in one_succ]
N.peano_ind [definition, in peano_ind]
N.peano_rec [definition, in peano_rec]
N.peano_rect_succ [lemma, in peano_rect_succ]
N.peano_rec_succ [lemma, in peano_rec_succ]
N.peano_rect_base [lemma, in peano_rect_base]
N.peano_rec_base [lemma, in peano_rec_base]
N.peano_rect [definition, in peano_rect]
N.pos [abbreviation, in pos]
N.pos_pred_shiftl_low [lemma, in pos_pred_shiftl_low]
N.pos_lxor_spec [lemma, in pos_lxor_spec]
N.pos_land_spec [lemma, in pos_land_spec]
N.pos_div_eucl [definition, in pos_div_eucl]
N.pos_div_eucl_remainder [lemma, in pos_div_eucl_remainder]
N.pos_ldiff_spec [lemma, in pos_ldiff_spec]
N.pos_lor_spec [lemma, in pos_lor_spec]
N.pos_pred_shiftl_high [lemma, in pos_pred_shiftl_high]
N.pos_pred_spec [lemma, in pos_pred_spec]
N.pos_div_eucl_spec [lemma, in pos_div_eucl_spec]
N.pos_pred_succ [lemma, in pos_pred_succ]
N.pow [definition, in pow]
N.pow_wd [definition, in pow_wd]
N.pow_0_r [lemma, in pow_0_r]
N.pow_succ_r [lemma, in pow_succ_r]
N.pow_neg_r [lemma, in pow_neg_r]
N.pred [definition, in pred]
N.pred_div2_up [lemma, in pred_div2_up]
N.pred_sub [lemma, in pred_sub]
N.pred_succ [lemma, in pred_succ]
N.pred_0 [definition, in pred_0]
N.pred_wd [definition, in pred_wd]
N.Private_BootStrap.le_0_l [lemma, in le_0_l]
N.Private_BootStrap.add_0_r [lemma, in add_0_r]
N.Private_BootStrap [module, in N.Private_BootStrap]
N.Private_BootStrap.add_assoc [lemma, in add_assoc]
N.Private_BootStrap.add_comm [lemma, in add_comm]
N.Private_BootStrap.sub_add [lemma, in sub_add]
N.Private_BootStrap.mul_comm [lemma, in mul_comm]
N.Private_BootStrap.add_lt_cancel_l [lemma, in add_lt_cancel_l]
N.Private_BootStrap.leb_spec [lemma, in leb_spec]
N.recursion [definition, in recursion]
N.recursion_wd [instance, in recursion_wd]
N.recursion_0 [lemma, in recursion_0]
N.recursion_succ [lemma, in recursion_succ]
N.shiftl [definition, in shiftl]
N.shiftl_succ_r [lemma, in shiftl_succ_r]
N.shiftl_spec_low [lemma, in shiftl_spec_low]
N.shiftl_nat [definition, in shiftl_nat]
N.shiftl_spec_high [lemma, in shiftl_spec_high]
N.shiftr [definition, in shiftr]
N.shiftr_nat [definition, in shiftr_nat]
N.shiftr_spec [lemma, in shiftr_spec]
N.shiftr_succ_r [lemma, in shiftr_succ_r]
N.size [definition, in size]
N.size_gt [lemma, in size_gt]
N.size_le [lemma, in size_le]
N.size_nat [definition, in size_nat]
N.size_log2 [lemma, in size_log2]
N.sqrt [definition, in sqrt]
N.sqrtrem [definition, in sqrtrem]
N.sqrtrem_sqrt [lemma, in sqrtrem_sqrt]
N.sqrtrem_spec [lemma, in sqrtrem_spec]
N.sqrt_spec [lemma, in sqrt_spec]
N.sqrt_neg [lemma, in sqrt_neg]
N.square [definition, in square]
N.square_spec [lemma, in square_spec]
N.sub [definition, in sub]
N.sub_wd [definition, in sub_wd]
N.sub_succ_r [lemma, in sub_succ_r]
N.sub_0_r [lemma, in sub_0_r]
N.succ [definition, in succ]
N.succ_pos [definition, in succ_pos]
N.succ_0_discr [lemma, in succ_0_discr]
N.succ_double_inj [lemma, in succ_double_inj]
N.succ_wd [definition, in succ_wd]
N.succ_pos_pred [lemma, in succ_pos_pred]
N.succ_double [definition, in succ_double]
N.succ_double_lt [lemma, in succ_double_lt]
N.succ_double_add [lemma, in succ_double_add]
N.succ_double_spec [lemma, in succ_double_spec]
N.succ_pos_spec [lemma, in succ_pos_spec]
N.succ_double_mul [lemma, in succ_double_mul]
N.t [definition, in t]
N.testbit [definition, in testbit]
N.testbit_even_0 [lemma, in testbit_even_0]
N.testbit_neg_r [lemma, in testbit_neg_r]
N.testbit_nat [definition, in testbit_nat]
N.testbit_even_succ [lemma, in testbit_even_succ]
N.testbit_odd_0 [lemma, in testbit_odd_0]
N.testbit_odd_succ [lemma, in testbit_odd_succ]
N.testbit_succ_r_div2 [lemma, in testbit_succ_r_div2]
N.testbit_wd [definition, in testbit_wd]
N.to_nat [definition, in to_nat]
N.two [definition, in two]
N.two_succ [lemma, in two_succ]
N.zero [definition, in zero]
_ <= _ < _ (N_scope) [notation, in :N_scope:x_'<='_x_'<'_x]
_ <= _ (N_scope) [notation, in :N_scope:x_'<='_x]
_ * _ (N_scope) [notation, in :N_scope:x_'*'_x]
_ - _ (N_scope) [notation, in :N_scope:x_'-'_x]
_ mod _ (N_scope) [notation, in :N_scope:x_'mod'_x]
_ / _ (N_scope) [notation, in :N_scope:x_'/'_x]
_ ?= _ (N_scope) [notation, in :N_scope:x_'?='_x]
_ >= _ (N_scope) [notation, in :N_scope:x_'>='_x]
_ < _ < _ (N_scope) [notation, in :N_scope:x_'<'_x_'<'_x]
( _ | _ ) (N_scope) [notation, in :N_scope:'('_x_'|'_x_')']
_ ^ _ (N_scope) [notation, in :N_scope:x_'^'_x]
_ <=? _ (N_scope) [notation, in :N_scope:x_'<=?'_x]
_ [notation, in :N_scope:x_']
_ =? _ (N_scope) [notation, in :N_scope:x_'=?'_x]
_ < _ (N_scope) [notation, in :N_scope:x_'<'_x]
_ + _ (N_scope) [notation, in :N_scope:x_'+'_x]
_ < _ <= _ (N_scope) [notation, in :N_scope:x_'<'_x_'<='_x]
_ <= _ <= _ (N_scope) [notation, in :N_scope:x_'<='_x_'<='_x]
_ > _ (N_scope) [notation, in :N_scope:x_'>'_x]
N0 [constructor, in N0]
N0 [abbreviation, in N0]
N0_less_1 [lemma, in N0_less_1]
N0_less_2 [lemma, in N0_less_2]
N2Bv [definition, in N2Bv]
N2Bv_N2Bv_gen [lemma, in N2Bv_N2Bv_gen]
N2Bv_Bv2N [lemma, in N2Bv_Bv2N]
N2Bv_gen [definition, in N2Bv_gen]
N2Bv_N2Bv_gen_above [lemma, in N2Bv_N2Bv_gen_above]
N2Nat [module, in N2Nat]
N2Nat.id [lemma, in id]
N2Nat.inj [lemma, in inj]
N2Nat.inj_max [lemma, in inj_max]
N2Nat.inj_succ_double [lemma, in inj_succ_double]
N2Nat.inj_mul [lemma, in inj_mul]
N2Nat.inj_double [lemma, in inj_double]
N2Nat.inj_iff [lemma, in inj_iff]
N2Nat.inj_iter [lemma, in inj_iter]
N2Nat.inj_add [lemma, in inj_add]
N2Nat.inj_div2 [lemma, in inj_div2]
N2Nat.inj_compare [lemma, in inj_compare]
N2Nat.inj_sub [lemma, in inj_sub]
N2Nat.inj_min [lemma, in inj_min]
N2Nat.inj_pred [lemma, in inj_pred]
N2Nat.inj_succ [lemma, in inj_succ]
N2Z [module, in N2Z]
N2Z.id [lemma, in id]
N2Z.inj [lemma, in inj]
N2Z.inj_max [lemma, in inj_max]
N2Z.inj_lt [lemma, in inj_lt]
N2Z.inj_pos [lemma, in inj_pos]
N2Z.inj_mul [lemma, in inj_mul]
N2Z.inj_abs_N [lemma, in inj_abs_N]
N2Z.inj_mod [lemma, in inj_mod]
N2Z.inj_pred_max [lemma, in inj_pred_max]
N2Z.inj_iff [lemma, in inj_iff]
N2Z.inj_quot [lemma, in inj_quot]
N2Z.inj_0 [lemma, in inj_0]
N2Z.inj_add [lemma, in inj_add]
N2Z.inj_div2 [lemma, in inj_div2]
N2Z.inj_ge [lemma, in inj_ge]
N2Z.inj_compare [lemma, in inj_compare]
N2Z.inj_sub [lemma, in inj_sub]
N2Z.inj_testbit [lemma, in inj_testbit]
N2Z.inj_min [lemma, in inj_min]
N2Z.inj_quot2 [lemma, in inj_quot2]
N2Z.inj_le [lemma, in inj_le]
N2Z.inj_pred [lemma, in inj_pred]
N2Z.inj_succ [lemma, in inj_succ]
N2Z.inj_div [lemma, in inj_div]
N2Z.inj_rem [lemma, in inj_rem]
N2Z.inj_pow [lemma, in inj_pow]
N2Z.inj_sub_max [lemma, in inj_sub_max]
N2Z.inj_gt [lemma, in inj_gt]
N2Z.is_nonneg [lemma, in is_nonneg]



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 _ other (18816 entries)
Notation 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 _ other (644 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 _ other (708 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 _ other (1456 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 _ other (407 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 _ other (8932 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 _ other (422 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 _ other (699 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 _ other (209 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 _ other (203 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 _ other (550 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 _ other (338 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 _ other (1235 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 _ other (2946 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 _ other (67 entries)