N (lemma)
NAddOrderProp.add_pos_l [in add_pos_l]
NAddOrderProp.add_pos_r [in add_pos_r]
NAddOrderProp.le_add_r [in le_add_r]
NAddOrderProp.lt_lt_add_l [in lt_lt_add_l]
NAddOrderProp.lt_lt_add_r [in lt_lt_add_r]
NAddProp.add_pred_r [in add_pred_r]
NAddProp.add_pred_l [in add_pred_l]
NAddProp.eq_add_1 [in eq_add_1]
NAddProp.eq_add_succ [in eq_add_succ]
NAddProp.eq_add_0 [in eq_add_0]
NAddProp.succ_add_discr [in succ_add_discr]
Nand_semantics [in Nand_semantics]
Nand_BVand [in Nand_BVand]
natlike_rec2 [in natlike_rec2]
natlike_rec [in natlike_rec]
natlike_ind [in natlike_ind]
natlike_rec3 [in natlike_rec3]
NatOrder.leb_total [in leb_total]
nat_of_P_gt_Gt_compare_morphism [in nat_of_P_gt_Gt_compare_morphism]
nat_of_P_lt_Lt_compare_complement_morphism [in nat_of_P_lt_Lt_compare_complement_morphism]
nat_compare_gt [in nat_compare_gt]
nat_iter_succ_r [in nat_iter_succ_r]
nat_iter_plus [in nat_iter_plus]
nat_compare_lt [in nat_compare_lt]
nat_compare_Gt_gt [in nat_compare_Gt_gt]
nat_total_order [in nat_total_order]
nat_compare_eq_iff [in nat_compare_eq_iff]
nat_of_P_lt_Lt_compare_morphism [in nat_of_P_lt_Lt_compare_morphism]
nat_ascii_embedding [in nat_ascii_embedding]
nat_double_ind [in nat_double_ind]
nat_compare_ge [in nat_compare_ge]
nat_compare_Lt_lt [in nat_compare_Lt_lt]
Nat_as_OT.lt_not_eq [in lt_not_eq]
Nat_as_OT.lt_trans [in lt_trans]
nat_case [in nat_case]
nat_compare_spec [in nat_compare_spec]
nat_compare_equiv [in nat_compare_equiv]
nat_compare_eq [in nat_compare_eq]
nat_of_P_minus_morphism [in nat_of_P_minus_morphism]
nat_N_Z [in nat_N_Z]
nat_compare_S [in nat_compare_S]
nat_compare_le [in nat_compare_le]
nat_iter_invariant [in nat_iter_invariant]
Nat.add_succ_l [in add_succ_l]
Nat.add_0_l [in add_0_l]
Nat.bi_induction [in bi_induction]
Nat.gcd_nonneg [in gcd_nonneg]
Nat.lt_irrefl [in lt_irrefl]
Nat.lt_eq_cases [in lt_eq_cases]
Nat.lt_succ_r [in lt_succ_r]
Nat.mul_succ_l [in mul_succ_l]
Nat.mul_0_l [in mul_0_l]
Nat.one_succ [in one_succ]
Nat.pow_neg_r [in pow_neg_r]
Nat.pred_succ [in pred_succ]
Nat.pred_0 [in pred_0]
Nat.recursion_0 [in recursion_0]
Nat.recursion_succ [in recursion_succ]
Nat.sqrt_neg [in sqrt_neg]
Nat.sub_succ_r [in sub_succ_r]
Nat.sub_0_r [in sub_0_r]
Nat.testbit_neg_r [in testbit_neg_r]
Nat.two_succ [in two_succ]
Nat2N.id [in id]
Nat2N.inj [in inj]
Nat2N.inj_max [in inj_max]
Nat2N.inj_succ_double [in inj_succ_double]
Nat2N.inj_mul [in inj_mul]
Nat2N.inj_double [in inj_double]
Nat2N.inj_iff [in inj_iff]
Nat2N.inj_iter [in inj_iter]
Nat2N.inj_add [in inj_add]
Nat2N.inj_div2 [in inj_div2]
Nat2N.inj_compare [in inj_compare]
Nat2N.inj_sub [in inj_sub]
Nat2N.inj_min [in inj_min]
Nat2N.inj_pred [in inj_pred]
Nat2N.inj_succ [in inj_succ]
Nat2Pos.id [in id]
Nat2Pos.id_max [in id_max]
Nat2Pos.inj [in inj]
Nat2Pos.inj_max [in inj_max]
Nat2Pos.inj_mul [in inj_mul]
Nat2Pos.inj_iff [in inj_iff]
Nat2Pos.inj_add [in inj_add]
Nat2Pos.inj_compare [in inj_compare]
Nat2Pos.inj_sub [in inj_sub]
Nat2Pos.inj_min [in inj_min]
Nat2Pos.inj_pred [in inj_pred]
Nat2Pos.inj_succ [in inj_succ]
Nat2Z.id [in id]
Nat2Z.inj [in inj]
Nat2Z.inj_max [in inj_max]
Nat2Z.inj_lt [in inj_lt]
Nat2Z.inj_abs_nat [in inj_abs_nat]
Nat2Z.inj_mul [in inj_mul]
Nat2Z.inj_pred_max [in inj_pred_max]
Nat2Z.inj_iff [in inj_iff]
Nat2Z.inj_0 [in inj_0]
Nat2Z.inj_add [in inj_add]
Nat2Z.inj_ge [in inj_ge]
Nat2Z.inj_compare [in inj_compare]
Nat2Z.inj_sub [in inj_sub]
Nat2Z.inj_min [in inj_min]
Nat2Z.inj_le [in inj_le]
Nat2Z.inj_pred [in inj_pred]
Nat2Z.inj_succ [in inj_succ]
Nat2Z.inj_sub_max [in inj_sub_max]
Nat2Z.inj_gt [in inj_gt]
Nat2Z.is_nonneg [in is_nonneg]
NBaseProp.case_analysis [in case_analysis]
NBaseProp.double_induction [in double_induction]
NBaseProp.eq_pred_0 [in eq_pred_0]
NBaseProp.induction [in induction]
NBaseProp.le_0_l [in le_0_l]
NBaseProp.neq_0_r [in neq_0_r]
NBaseProp.neq_0 [in neq_0]
NBaseProp.neq_succ_0 [in neq_succ_0]
NBaseProp.neq_0_succ [in neq_0_succ]
NBaseProp.pair_induction [in pair_induction]
NBaseProp.pred_inj [in pred_inj]
NBaseProp.succ_pred [in succ_pred]
NBaseProp.two_dim_induction [in two_dim_induction]
NBaseProp.zero_or_succ [in zero_or_succ]
NBitsProp.add_bit0 [in add_bit0]
NBitsProp.add_bit1 [in add_bit1]
NBitsProp.add_b2n_double_div2 [in add_b2n_double_div2]
NBitsProp.add_nocarry_mod_lt_pow2 [in add_nocarry_mod_lt_pow2]
NBitsProp.add_carry_div2 [in add_carry_div2]
NBitsProp.add_lnot_diag_low [in add_lnot_diag_low]
NBitsProp.add_nocarry_lxor [in add_nocarry_lxor]
NBitsProp.add_nocarry_lt_pow2 [in add_nocarry_lt_pow2]
NBitsProp.add_carry_bits [in add_carry_bits]
NBitsProp.add_b2n_double_bit0 [in add_b2n_double_bit0]
NBitsProp.add3_bits_div2 [in add3_bits_div2]
NBitsProp.add3_bit0 [in add3_bit0]
NBitsProp.are_bits [in are_bits]
NBitsProp.bits_above_log2 [in bits_above_log2]
NBitsProp.bits_0 [in bits_0]
NBitsProp.bits_inj_0 [in bits_inj_0]
NBitsProp.bits_inj_iff [in bits_inj_iff]
NBitsProp.bits_inj [in bits_inj]
NBitsProp.bit_log2 [in bit_log2]
NBitsProp.bit0_eqb [in bit0_eqb]
NBitsProp.bit0_odd [in bit0_odd]
NBitsProp.bit0_mod [in bit0_mod]
NBitsProp.b2n_bit0 [in b2n_bit0]
NBitsProp.b2n_inj [in b2n_inj]
NBitsProp.b2n_div2 [in b2n_div2]
NBitsProp.clearbit_spec' [in clearbit_spec']
NBitsProp.clearbit_iff [in clearbit_iff]
NBitsProp.clearbit_eq [in clearbit_eq]
NBitsProp.clearbit_neq [in clearbit_neq]
NBitsProp.clearbit_eqb [in clearbit_eqb]
NBitsProp.div_pow2_bits [in div_pow2_bits]
NBitsProp.div2_div [in div2_div]
NBitsProp.div2_bits [in div2_bits]
NBitsProp.div2_odd [in div2_odd]
NBitsProp.double_bits_succ [in double_bits_succ]
NBitsProp.exists_div2 [in exists_div2]
NBitsProp.land_comm [in land_comm]
NBitsProp.land_assoc [in land_assoc]
NBitsProp.land_0_l [in land_0_l]
NBitsProp.land_ones_low [in land_ones_low]
NBitsProp.land_ldiff [in land_ldiff]
NBitsProp.land_lnot_diag [in land_lnot_diag]
NBitsProp.land_lor_distr_r [in land_lor_distr_r]
NBitsProp.land_ones [in land_ones]
NBitsProp.land_diag [in land_diag]
NBitsProp.land_lnot_diag_low [in land_lnot_diag_low]
NBitsProp.land_0_r [in land_0_r]
NBitsProp.land_lor_distr_l [in land_lor_distr_l]
NBitsProp.ldiff_land_low [in ldiff_land_low]
NBitsProp.ldiff_ldiff_l [in ldiff_ldiff_l]
NBitsProp.ldiff_ones_r_low [in ldiff_ones_r_low]
NBitsProp.ldiff_ones_r [in ldiff_ones_r]
NBitsProp.ldiff_ones_l_low [in ldiff_ones_l_low]
NBitsProp.ldiff_diag [in ldiff_diag]
NBitsProp.ldiff_le [in ldiff_le]
NBitsProp.ldiff_0_l [in ldiff_0_l]
NBitsProp.ldiff_0_r [in ldiff_0_r]
NBitsProp.lnot_ldiff_low [in lnot_ldiff_low]
NBitsProp.lnot_lor_low [in lnot_lor_low]
NBitsProp.lnot_land_low [in lnot_land_low]
NBitsProp.lnot_spec_high [in lnot_spec_high]
NBitsProp.lnot_lxor_l [in lnot_lxor_l]
NBitsProp.lnot_ones [in lnot_ones]
NBitsProp.lnot_0_l [in lnot_0_l]
NBitsProp.lnot_lxor_r [in lnot_lxor_r]
NBitsProp.lnot_involutive [in lnot_involutive]
NBitsProp.lnot_sub_low [in lnot_sub_low]
NBitsProp.lnot_spec_low [in lnot_spec_low]
NBitsProp.log2_lor [in log2_lor]
NBitsProp.log2_shiftr [in log2_shiftr]
NBitsProp.log2_lxor [in log2_lxor]
NBitsProp.log2_bits_unique [in log2_bits_unique]
NBitsProp.log2_shiftl [in log2_shiftl]
NBitsProp.log2_land [in log2_land]
NBitsProp.lor_comm [in lor_comm]
NBitsProp.lor_eq_0_iff [in lor_eq_0_iff]
NBitsProp.lor_ldiff_and [in lor_ldiff_and]
NBitsProp.lor_land_distr_r [in lor_land_distr_r]
NBitsProp.lor_eq_0_l [in lor_eq_0_l]
NBitsProp.lor_land_distr_l [in lor_land_distr_l]
NBitsProp.lor_lnot_diag [in lor_lnot_diag]
NBitsProp.lor_0_r [in lor_0_r]
NBitsProp.lor_ones_low [in lor_ones_low]
NBitsProp.lor_assoc [in lor_assoc]
NBitsProp.lor_diag [in lor_diag]
NBitsProp.lor_0_l [in lor_0_l]
NBitsProp.lor_lnot_diag_low [in lor_lnot_diag_low]
NBitsProp.lxor_lnot_lnot [in lxor_lnot_lnot]
NBitsProp.lxor_0_r [in lxor_0_r]
NBitsProp.lxor_0_l [in lxor_0_l]
NBitsProp.lxor_lor [in lxor_lor]
NBitsProp.lxor_eq_0_iff [in lxor_eq_0_iff]
NBitsProp.lxor_comm [in lxor_comm]
NBitsProp.lxor_assoc [in lxor_assoc]
NBitsProp.lxor_eq [in lxor_eq]
NBitsProp.lxor_nilpotent [in lxor_nilpotent]
NBitsProp.mod_pow2_bits_high [in mod_pow2_bits_high]
NBitsProp.mod_pow2_bits_low [in mod_pow2_bits_low]
NBitsProp.mul_pow2_bits_high [in mul_pow2_bits_high]
NBitsProp.mul_pow2_bits_low [in mul_pow2_bits_low]
NBitsProp.mul_pow2_bits_add [in mul_pow2_bits_add]
NBitsProp.nocarry_equiv [in nocarry_equiv]
NBitsProp.ones_mod_pow2 [in ones_mod_pow2]
NBitsProp.ones_div_pow2 [in ones_div_pow2]
NBitsProp.ones_spec_iff [in ones_spec_iff]
NBitsProp.ones_add [in ones_add]
NBitsProp.ones_equiv [in ones_equiv]
NBitsProp.ones_spec_low [in ones_spec_low]
NBitsProp.ones_spec_high [in ones_spec_high]
NBitsProp.pow_div_l [in pow_div_l]
NBitsProp.pow_sub_r [in pow_sub_r]
NBitsProp.pow2_bits_eqb [in pow2_bits_eqb]
NBitsProp.pow2_bits_false [in pow2_bits_false]
NBitsProp.pow2_bits_true [in pow2_bits_true]
NBitsProp.setbit_neq [in setbit_neq]
NBitsProp.setbit_eqb [in setbit_eqb]
NBitsProp.setbit_eq [in setbit_eq]
NBitsProp.setbit_spec' [in setbit_spec']
NBitsProp.setbit_iff [in setbit_iff]
NBitsProp.shiftl_land [in shiftl_land]
NBitsProp.shiftl_lxor [in shiftl_lxor]
NBitsProp.shiftl_1_l [in shiftl_1_l]
NBitsProp.shiftl_eq_0_iff [in shiftl_eq_0_iff]
NBitsProp.shiftl_0_l [in shiftl_0_l]
NBitsProp.shiftl_mul_pow2 [in shiftl_mul_pow2]
NBitsProp.shiftl_ldiff [in shiftl_ldiff]
NBitsProp.shiftl_0_r [in shiftl_0_r]
NBitsProp.shiftl_shiftl [in shiftl_shiftl]
NBitsProp.shiftl_spec_alt [in shiftl_spec_alt]
NBitsProp.shiftl_spec_high' [in shiftl_spec_high']
NBitsProp.shiftl_lor [in shiftl_lor]
NBitsProp.shiftr_div_pow2 [in shiftr_div_pow2]
NBitsProp.shiftr_ldiff [in shiftr_ldiff]
NBitsProp.shiftr_lxor [in shiftr_lxor]
NBitsProp.shiftr_0_l [in shiftr_0_l]
NBitsProp.shiftr_spec' [in shiftr_spec']
NBitsProp.shiftr_shiftl_l [in shiftr_shiftl_l]
NBitsProp.shiftr_eq_0 [in shiftr_eq_0]
NBitsProp.shiftr_shiftl_r [in shiftr_shiftl_r]
NBitsProp.shiftr_land [in shiftr_land]
NBitsProp.shiftr_lor [in shiftr_lor]
NBitsProp.shiftr_0_r [in shiftr_0_r]
NBitsProp.shiftr_shiftr [in shiftr_shiftr]
NBitsProp.shiftr_eq_0_iff [in shiftr_eq_0_iff]
NBitsProp.sub_nocarry_ldiff [in sub_nocarry_ldiff]
NBitsProp.testbit_0_r [in testbit_0_r]
NBitsProp.testbit_true [in testbit_true]
NBitsProp.testbit_eqb [in testbit_eqb]
NBitsProp.testbit_false [in testbit_false]
NBitsProp.testbit_unique [in testbit_unique]
NBitsProp.testbit_spec [in testbit_spec]
NBitsProp.testbit_spec' [in testbit_spec']
NBitsProp.testbit_succ_r [in testbit_succ_r]
NBitsProp.testbit_odd [in testbit_odd]
Nbit_faithful [in Nbit_faithful]
Nbit_faithful_iff [in Nbit_faithful_iff]
Nbit_Ntestbit [in Nbit_Ntestbit]
Nbit_Nsize [in Nbit_Nsize]
Nbit_Bth [in Nbit_Bth]
Nbit0_less [in Nbit0_less]
Nbit0_neq [in Nbit0_neq]
Nbit0_correct [in Nbit0_correct]
Nbit0_gt [in Nbit0_gt]
Nbit0_Blow [in Nbit0_Blow]
Ncompare_Lt_Nltb [in Ncompare_Lt_Nltb]
Ncompare_Gt_Nltb [in Ncompare_Gt_Nltb]
Ncompare_antisym [in Ncompare_antisym]
Ncompare_Neqb [in Ncompare_Neqb]
NdefOpsProp.def_add_0_l [in def_add_0_l]
NdefOpsProp.def_add_add [in def_add_add]
NdefOpsProp.def_add_succ_l [in def_add_succ_l]
NdefOpsProp.def_mul_0_r [in def_mul_0_r]
NdefOpsProp.def_mul_succ_r [in def_mul_succ_r]
NdefOpsProp.def_mul_mul [in def_mul_mul]
NdefOpsProp.even_0 [in even_0]
NdefOpsProp.even_succ [in even_succ]
NdefOpsProp.half_aux_0 [in half_aux_0]
NdefOpsProp.half_aux_succ [in half_aux_succ]
NdefOpsProp.half_aux_spec2 [in half_aux_spec2]
NdefOpsProp.half_upper_bound [in half_upper_bound]
NdefOpsProp.half_aux_spec [in half_aux_spec]
NdefOpsProp.half_0 [in half_0]
NdefOpsProp.half_1 [in half_1]
NdefOpsProp.half_nz [in half_nz]
NdefOpsProp.half_lower_bound [in half_lower_bound]
NdefOpsProp.half_double [in half_double]
NdefOpsProp.half_decrease [in half_decrease]
NdefOpsProp.if_zero_0 [in if_zero_0]
NdefOpsProp.if_zero_succ [in if_zero_succ]
NdefOpsProp.log_init [in log_init]
NdefOpsProp.log_step [in log_step]
NdefOpsProp.log_good_step [in log_good_step]
NdefOpsProp.ltb_step [in ltb_step]
NdefOpsProp.ltb_ge [in ltb_ge]
NdefOpsProp.ltb_0 [in ltb_0]
NdefOpsProp.ltb_0_succ [in ltb_0_succ]
NdefOpsProp.ltb_base [in ltb_base]
NdefOpsProp.ltb_lt [in ltb_lt]
NdefOpsProp.pow_succ [in pow_succ]
NdefOpsProp.pow_0 [in pow_0]
NdefOpsProp.pow2_log [in pow2_log]
NdefOpsProp.succ_ltb_mono [in succ_ltb_mono]
Ndiff_semantics [in Ndiff_semantics]
NDivProp.add_mod_idemp_r [in add_mod_idemp_r]
NDivProp.add_mod_idemp_l [in add_mod_idemp_l]
NDivProp.add_mod [in add_mod]
NDivProp.div_mod_unique [in div_mod_unique]
NDivProp.div_unique [in div_unique]
NDivProp.div_small_iff [in div_small_iff]
NDivProp.div_mul_le [in div_mul_le]
NDivProp.div_mul [in div_mul]
NDivProp.div_0_l [in div_0_l]
NDivProp.div_div [in div_div]
NDivProp.div_add [in div_add]
NDivProp.div_1_l [in div_1_l]
NDivProp.div_exact [in div_exact]
NDivProp.div_le_mono [in div_le_mono]
NDivProp.div_same [in div_same]
NDivProp.div_unique_exact [in div_unique_exact]
NDivProp.div_mul_cancel_r [in div_mul_cancel_r]
NDivProp.div_le_compat_l [in div_le_compat_l]
NDivProp.div_le_upper_bound [in div_le_upper_bound]
NDivProp.div_lt [in div_lt]
NDivProp.div_mul_cancel_l [in div_mul_cancel_l]
NDivProp.div_le_lower_bound [in div_le_lower_bound]
NDivProp.div_small [in div_small]
NDivProp.div_str_pos_iff [in div_str_pos_iff]
NDivProp.div_str_pos [in div_str_pos]
NDivProp.div_1_r [in div_1_r]
NDivProp.div_lt_upper_bound [in div_lt_upper_bound]
NDivProp.div_add_l [in div_add_l]
NDivProp.mod_1_r [in mod_1_r]
NDivProp.mod_small_iff [in mod_small_iff]
NDivProp.mod_mul_r [in mod_mul_r]
NDivProp.mod_unique [in mod_unique]
NDivProp.mod_upper_bound [in mod_upper_bound]
NDivProp.mod_le [in mod_le]
NDivProp.mod_add [in mod_add]
NDivProp.mod_small [in mod_small]
NDivProp.mod_mod [in mod_mod]
NDivProp.mod_divides [in mod_divides]
NDivProp.mod_eq [in mod_eq]
NDivProp.mod_0_l [in mod_0_l]
NDivProp.mod_mul [in mod_mul]
NDivProp.mod_same [in mod_same]
NDivProp.mod_1_l [in mod_1_l]
NDivProp.mul_succ_div_gt [in mul_succ_div_gt]
NDivProp.mul_mod [in mul_mod]
NDivProp.mul_mod_distr_r [in mul_mod_distr_r]
NDivProp.mul_mod_distr_l [in mul_mod_distr_l]
NDivProp.mul_mod_idemp_r [in mul_mod_idemp_r]
NDivProp.mul_mod_idemp_l [in mul_mod_idemp_l]
NDivProp.mul_div_le [in mul_div_le]
Ndiv2_double_plus_one [in Ndiv2_double_plus_one]
Ndiv2_bit_eq [in Ndiv2_bit_eq]
Ndiv2_correct [in Ndiv2_correct]
Ndiv2_double [in Ndiv2_double]
Ndiv2_eq [in Ndiv2_eq]
Ndiv2_bit_neq [in Ndiv2_bit_neq]
Ndiv2_neq [in Ndiv2_neq]
Ndouble_bit0 [in Ndouble_bit0]
Ndouble_plus_one_bit0 [in Ndouble_plus_one_bit0]
Ndouble_or_double_plus_un [in Ndouble_or_double_plus_un]
negative_derivative [in negative_derivative]
negb_true_iff [in negb_true_iff]
negb_orb [in negb_orb]
negb_prop_elim [in negb_prop_elim]
negb_sym [in negb_sym]
negb_prop_involutive [in negb_prop_involutive]
negb_andb [in negb_andb]
negb_false_iff [in negb_false_iff]
negb_prop_intro [in negb_prop_intro]
negb_involutive [in negb_involutive]
negb_if [in negb_if]
negb_involutive_reverse [in negb_involutive_reverse]
negb_prop_classical [in negb_prop_classical]
negb_xorb_r [in negb_xorb_r]
negb_xorb_l [in negb_xorb_l]
neg_cos [in neg_cos]
neg_sin [in neg_sin]
neg_false [in neg_false]
neg_pos_Rsqr_le [in neg_pos_Rsqr_le]
neighbourhood_P1 [in neighbourhood_P1]
Neqb_complete [in Neqb_complete]
Neqb_Ncompare [in Neqb_Ncompare]
nequiv_equiv_trans [in nequiv_equiv_trans]
neq_0_lt [in neq_0_lt]
Neven_not_double_plus_one [in Neven_not_double_plus_one]
Newman [in Newman]
NewtonInt_P4 [in NewtonInt_P4]
NewtonInt_P6 [in NewtonInt_P6]
NewtonInt_P7 [in NewtonInt_P7]
NewtonInt_P5 [in NewtonInt_P5]
NewtonInt_P1 [in NewtonInt_P1]
NewtonInt_P9 [in NewtonInt_P9]
NewtonInt_P2 [in NewtonInt_P2]
NewtonInt_P3 [in NewtonInt_P3]
NewtonInt_P8 [in NewtonInt_P8]
NGcdProp.bezout_1_gcd [in bezout_1_gcd]
NGcdProp.divide_mul_split [in divide_mul_split]
NGcdProp.divide_add_cancel_r [in divide_add_cancel_r]
NGcdProp.divide_sub_r [in divide_sub_r]
NGcdProp.gauss [in gauss]
NGcdProp.gcd_mul_mono_l [in gcd_mul_mono_l]
NGcdProp.gcd_add_mult_diag_r [in gcd_add_mult_diag_r]
NGcdProp.gcd_bezout_pos [in gcd_bezout_pos]
NGcdProp.gcd_mul_mono_r [in gcd_mul_mono_r]
NGcdProp.gcd_sub_diag_r [in gcd_sub_diag_r]
NGcdProp.gcd_bezout_pos_pos [in gcd_bezout_pos_pos]
NGcdProp.gcd_add_diag_r [in gcd_add_diag_r]
NGcdProp.gcd_bezout [in gcd_bezout]
nil_cons [in nil_cons]
ni_le_min_2 [in ni_le_min_2]
ni_le_min_1 [in ni_le_min_1]
ni_min_idemp [in ni_min_idemp]
ni_le_antisym [in ni_le_antisym]
ni_le_trans [in ni_le_trans]
ni_min_inf_l [in ni_min_inf_l]
ni_min_comm [in ni_min_comm]
ni_min_case [in ni_min_case]
ni_min_assoc [in ni_min_assoc]
ni_le_min_induc [in ni_le_min_induc]
ni_le_total [in ni_le_total]
ni_le_le [in ni_le_le]
ni_min_O_r [in ni_min_O_r]
ni_le_refl [in ni_le_refl]
ni_min_O_l [in ni_min_O_l]
ni_min_inf_r [in ni_min_inf_r]
NLcmProp.divide_lcm_l [in divide_lcm_l]
NLcmProp.divide_lcm_iff [in divide_lcm_iff]
NLcmProp.divide_lcm_r [in divide_lcm_r]
NLcmProp.divide_div [in divide_div]
NLcmProp.divide_lcm_eq_r [in divide_lcm_eq_r]
NLcmProp.divide_div_mul_exact [in divide_div_mul_exact]
NLcmProp.gcd_1_lcm_mul [in gcd_1_lcm_mul]
NLcmProp.gcd_div_factor [in gcd_div_factor]
NLcmProp.gcd_div_gcd [in gcd_div_gcd]
NLcmProp.gcd_div_swap [in gcd_div_swap]
NLcmProp.gcd_mod [in gcd_mod]
NLcmProp.lcm_1_l [in lcm_1_l]
NLcmProp.lcm_0_l [in lcm_0_l]
NLcmProp.lcm_0_r [in lcm_0_r]
NLcmProp.lcm_least [in lcm_least]
NLcmProp.lcm_equiv1 [in lcm_equiv1]
NLcmProp.lcm_1_r [in lcm_1_r]
NLcmProp.lcm_mul_mono_l [in lcm_mul_mono_l]
NLcmProp.lcm_unique_alt [in lcm_unique_alt]
NLcmProp.lcm_eq_0 [in lcm_eq_0]
NLcmProp.lcm_unique [in lcm_unique]
NLcmProp.lcm_divide_iff [in lcm_divide_iff]
NLcmProp.lcm_assoc [in lcm_assoc]
NLcmProp.lcm_equiv2 [in lcm_equiv2]
NLcmProp.lcm_comm [in lcm_comm]
NLcmProp.lcm_mul_mono_r [in lcm_mul_mono_r]
NLcmProp.lcm_diag [in lcm_diag]
NLcmProp.mod_divide [in mod_divide]
Nleb_double_mono_conv [in Nleb_double_mono_conv]
Nleb_double_plus_one_mono_conv [in Nleb_double_plus_one_mono_conv]
Nleb_alt [in Nleb_alt]
Nleb_Nle [in Nleb_Nle]
Nleb_refl [in Nleb_refl]
Nleb_antisym [in Nleb_antisym]
Nleb_double_mono [in Nleb_double_mono]
Nleb_trans [in Nleb_trans]
Nleb_ltb_trans [in Nleb_ltb_trans]
Nleb_double_plus_one_mono [in Nleb_double_plus_one_mono]
Nless_not_refl [in Nless_not_refl]
Nless_z [in Nless_z]
Nless_def_3 [in Nless_def_3]
Nless_def_2 [in Nless_def_2]
Nless_def_4 [in Nless_def_4]
Nless_def_1 [in Nless_def_1]
Nless_total [in Nless_total]
Nless_trans [in Nless_trans]
Nltb_double_mono_conv [in Nltb_double_mono_conv]
Nltb_double_mono [in Nltb_double_mono]
Nltb_trans [in Nltb_trans]
Nltb_double_plus_one_mono_conv [in Nltb_double_plus_one_mono_conv]
Nltb_leb_weak [in Nltb_leb_weak]
Nltb_double_plus_one_mono [in Nltb_double_plus_one_mono]
Nltb_leb_trans [in Nltb_leb_trans]
Nltb_Ncompare [in Nltb_Ncompare]
NMaxMinProp.add_max_distr_r [in add_max_distr_r]
NMaxMinProp.add_min_distr_r [in add_min_distr_r]
NMaxMinProp.add_min_distr_l [in add_min_distr_l]
NMaxMinProp.add_max_distr_l [in add_max_distr_l]
NMaxMinProp.max_0_l [in max_0_l]
NMaxMinProp.max_0_r [in max_0_r]
NMaxMinProp.min_0_l [in min_0_l]
NMaxMinProp.min_0_r [in min_0_r]
NMaxMinProp.mul_min_distr_r [in mul_min_distr_r]
NMaxMinProp.mul_max_distr_r [in mul_max_distr_r]
NMaxMinProp.mul_max_distr_l [in mul_max_distr_l]
NMaxMinProp.mul_min_distr_l [in mul_min_distr_l]
NMaxMinProp.sub_max_distr_r [in sub_max_distr_r]
NMaxMinProp.sub_max_distr_l [in sub_max_distr_l]
NMaxMinProp.sub_min_distr_l [in sub_min_distr_l]
NMaxMinProp.sub_min_distr_r [in sub_min_distr_r]
NMaxMinProp.succ_min_distr [in succ_min_distr]
NMaxMinProp.succ_max_distr [in succ_max_distr]
Nmin_le_1 [in Nmin_le_1]
Nmin_le_2 [in Nmin_le_2]
Nmin_le_3 [in Nmin_le_3]
Nmin_lt_4 [in Nmin_lt_4]
Nmin_le_4 [in Nmin_le_4]
Nmin_lt_3 [in Nmin_lt_3]
Nmin_le_5 [in Nmin_le_5]
NMulOrderProp.eq_mul_1 [in eq_mul_1]
NMulOrderProp.lt_0_mul' [in lt_0_mul']
NMulOrderProp.mul_le_mono [in mul_le_mono]
NMulOrderProp.mul_lt_mono [in mul_lt_mono]
NMulOrderProp.mul_le_mono_r [in mul_le_mono_r]
NMulOrderProp.mul_le_mono_l [in mul_le_mono_l]
NMulOrderProp.square_lt_mono [in square_lt_mono]
NMulOrderProp.square_le_mono [in square_le_mono]
Nmult_plus_distr_l [in Nmult_plus_distr_l]
Nmult_reg_r [in Nmult_reg_r]
Nmult_Sn_m [in Nmult_Sn_m]
Nneg_bit0_2 [in Nneg_bit0_2]
Nneg_bit0_1 [in Nneg_bit0_1]
Nneg_bit0 [in Nneg_bit0]
Nneq_elim [in Nneq_elim]
Nnot_div2_not_double [in Nnot_div2_not_double]
Nnot_div2_not_double_plus_one [in Nnot_div2_not_double_plus_one]
NNPP [in NNPP]
Nodd_not_double [in Nodd_not_double]
NodepOfDep.add_1 [in add_1]
NodepOfDep.add_2 [in add_2]
NodepOfDep.add_3 [in add_3]
NodepOfDep.cardinal_1 [in cardinal_1]
NodepOfDep.choose_3 [in choose_3]
NodepOfDep.choose_1 [in choose_1]
NodepOfDep.choose_2 [in choose_2]
NodepOfDep.compat_P_aux [in compat_P_aux]
NodepOfDep.diff_2 [in diff_2]
NodepOfDep.diff_1 [in diff_1]
NodepOfDep.diff_3 [in diff_3]
NodepOfDep.elements_3w [in elements_3w]
NodepOfDep.elements_3 [in elements_3]
NodepOfDep.elements_1 [in elements_1]
NodepOfDep.elements_2 [in elements_2]
NodepOfDep.empty_1 [in empty_1]
NodepOfDep.equal_2 [in equal_2]
NodepOfDep.equal_1 [in equal_1]
NodepOfDep.exists_1 [in exists_1]
NodepOfDep.exists_2 [in exists_2]
NodepOfDep.filter_1 [in filter_1]
NodepOfDep.filter_3 [in filter_3]
NodepOfDep.filter_2 [in filter_2]
NodepOfDep.fold_1 [in fold_1]
NodepOfDep.for_all_1 [in for_all_1]
NodepOfDep.for_all_2 [in for_all_2]
NodepOfDep.inter_3 [in inter_3]
NodepOfDep.inter_2 [in inter_2]
NodepOfDep.inter_1 [in inter_1]
NodepOfDep.is_empty_1 [in is_empty_1]
NodepOfDep.is_empty_2 [in is_empty_2]
NodepOfDep.max_elt_1 [in max_elt_1]
NodepOfDep.max_elt_3 [in max_elt_3]
NodepOfDep.max_elt_2 [in max_elt_2]
NodepOfDep.mem_1 [in mem_1]
NodepOfDep.mem_2 [in mem_2]
NodepOfDep.min_elt_3 [in min_elt_3]
NodepOfDep.min_elt_2 [in min_elt_2]
NodepOfDep.min_elt_1 [in min_elt_1]
NodepOfDep.partition_1 [in partition_1]
NodepOfDep.partition_2 [in partition_2]
NodepOfDep.remove_2 [in remove_2]
NodepOfDep.remove_1 [in remove_1]
NodepOfDep.remove_3 [in remove_3]
NodepOfDep.singleton_1 [in singleton_1]
NodepOfDep.singleton_2 [in singleton_2]
NodepOfDep.subset_2 [in subset_2]
NodepOfDep.subset_1 [in subset_1]
NodepOfDep.union_1 [in union_1]
NodepOfDep.union_2 [in union_2]
NodepOfDep.union_3 [in union_3]
NoDupA_swap [in NoDupA_swap]
NoDupA_equivlistA_permut [in NoDupA_equivlistA_permut]
NoDupA_app [in NoDupA_app]
NoDupA_split [in NoDupA_split]
NoDupA_rev [in NoDupA_rev]
NoDupA_equivlistA_PermutationA [in NoDupA_equivlistA_PermutationA]
NoDupA_altdef [in NoDupA_altdef]
NoDupA_singleton [in NoDupA_singleton]
NoDup_Permutation [in NoDup_Permutation]
NoDup_remove_2 [in NoDup_remove_2]
NoDup_remove_1 [in NoDup_remove_1]
NoDup_permut [in NoDup_permut]
Noetherian_contains_Noetherian [in Noetherian_contains_Noetherian]
nonneg_derivative_1 [in nonneg_derivative_1]
nonneg_derivative_0 [in nonneg_derivative_0]
nonpos_derivative_1 [in nonpos_derivative_1]
nonpos_derivative_0 [in nonpos_derivative_0]
Non_disjoint_union' [in Non_disjoint_union']
non_dep_dep_functional_choice [in non_dep_dep_functional_choice]
non_dep_dep_functional_rel_reification [in non_dep_dep_functional_rel_reification]
Non_disjoint_union [in Non_disjoint_union]
Noone_in_empty [in Noone_in_empty]
NOrderProp.eq_0_gt_0_cases [in eq_0_gt_0_cases]
NOrderProp.le_pred_le_succ [in le_pred_le_succ]
NOrderProp.le_le_pred [in le_le_pred]
NOrderProp.le_ind_rel [in le_ind_rel]
NOrderProp.le_1_r [in le_1_r]
NOrderProp.le_0_r [in le_0_r]
NOrderProp.le_pred_le [in le_pred_le]
NOrderProp.le_succ_le_pred [in le_succ_le_pred]
NOrderProp.le_pred_l [in le_pred_l]
NOrderProp.lt_1_l' [in lt_1_l']
NOrderProp.lt_1_r [in lt_1_r]
NOrderProp.lt_pred_le [in lt_pred_le]
NOrderProp.lt_pred_l [in lt_pred_l]
NOrderProp.lt_pred_lt [in lt_pred_lt]
NOrderProp.lt_le_pred [in lt_le_pred]
NOrderProp.lt_lt_0 [in lt_lt_0]
NOrderProp.lt_succ_lt_pred [in lt_succ_lt_pred]
NOrderProp.lt_ind_rel [in lt_ind_rel]
NOrderProp.lt_0_succ [in lt_0_succ]
NOrderProp.lt_lt_pred [in lt_lt_pred]
NOrderProp.lt_wf_0 [in lt_wf_0]
NOrderProp.lt_pred_lt_succ [in lt_pred_lt_succ]
NOrderProp.neq_0_lt_0 [in neq_0_lt_0]
NOrderProp.nle_succ_0 [in nle_succ_0]
NOrderProp.nlt_0_r [in nlt_0_r]
NOrderProp.pred_lt_mono [in pred_lt_mono]
NOrderProp.pred_le_mono [in pred_le_mono]
NOrderProp.succ_pred_pos [in succ_pred_pos]
NOrderProp.zero_one [in zero_one]
Nor_semantics [in Nor_semantics]
not_and_or [in not_and_or]
not_Zeq_inf [in not_Zeq_inf]
not_prime_divide [in not_prime_divide]
not_gt [in not_gt]
not_not_classic_set [in not_not_classic_set]
not_and [in not_and]
not_0_INR [in not_0_INR]
not_injective_elim [in not_injective_elim]
not_iff [in not_iff]
not_imply_elim [in not_imply_elim]
not_Zeq [in not_Zeq]
not_not_iff [in not_not_iff]
not_imp_iff [in not_imp_iff]
not_INR [in not_INR]
not_identity_sym [in not_identity_sym]
not_included_empty_Inhabited [in not_included_empty_Inhabited]
not_imp_rev_iff [in not_imp_rev_iff]
not_or_and [in not_or_and]
not_0_IZR [in not_0_IZR]
not_1_INR [in not_1_INR]
not_has_fixpoint [in not_has_fixpoint]
not_Rlt [in not_Rlt]
not_even_and_odd [in not_even_and_odd]
not_SIncl_empty [in not_SIncl_empty]
not_imply_elim2 [in not_imply_elim2]
not_or [in not_or]
not_Empty_Add [in not_Empty_Add]
not_or_iff [in not_or_iff]
not_false_iff [in not_false_iff]
not_true_iff [in not_true_iff]
not_prime_1 [in not_prime_1]
not_le [in not_le]
not_Zne [in not_Zne]
not_false_iff_true [in not_false_iff_true]
not_not_archimedean [in not_not_archimedean]
not_ex_not_all [in not_ex_not_all]
not_ex_not_all [in not_ex_not_all]
not_false_is_true [in not_false_is_true]
not_lt [in not_lt]
not_eq_sym [in not_eq_sym]
not_eq [in not_eq]
not_prime_0 [in not_prime_0]
not_all_not_ex [in not_all_not_ex]
not_all_not_ex [in not_all_not_ex]
not_empty_Inhabited [in not_empty_Inhabited]
not_not [in not_not]
not_all_ex_not [in not_all_ex_not]
not_all_ex_not [in not_all_ex_not]
not_imp [in not_imp]
not_eq_S [in not_eq_S]
not_ex_all_not [in not_ex_all_not]
not_ex_all_not [in not_ex_all_not]
not_rel_prime_0 [in not_rel_prime_0]
not_true_is_false [in not_true_is_false]
not_and_iff [in not_and_iff]
not_ge [in not_ge]
not_true_iff_false [in not_true_iff_false]
not_le_minus_0 [in not_le_minus_0]
no_fixpoint_negb [in no_fixpoint_negb]
NParityProp.even_sub [in even_sub]
NParityProp.even_pred [in even_pred]
NParityProp.odd_sub [in odd_sub]
NParityProp.odd_pred [in odd_pred]
Npdist_eq_1 [in Npdist_eq_1]
Npdist_comm [in Npdist_comm]
Npdist_ultra [in Npdist_ultra]
Npdist_eq_2 [in Npdist_eq_2]
Nplength_first_one [in Nplength_first_one]
Nplength_infty [in Nplength_infty]
Nplength_ultra_1 [in Nplength_ultra_1]
Nplength_lb [in Nplength_lb]
Nplength_zeros [in Nplength_zeros]
Nplength_ub [in Nplength_ub]
Nplength_one [in Nplength_one]
Nplength_ultra [in Nplength_ultra]
Nplus_reg_l [in Nplus_reg_l]
NPowProp.even_pow [in even_pow]
NPowProp.odd_pow [in odd_pow]
NPowProp.pow_le_mono_r [in pow_le_mono_r]
NPowProp.pow_inj_l [in pow_inj_l]
NPowProp.pow_le_mono_l_iff [in pow_le_mono_l_iff]
NPowProp.pow_nonzero [in pow_nonzero]
NPowProp.pow_lt_mono_l [in pow_lt_mono_l]
NPowProp.pow_le_mono_r_iff [in pow_le_mono_r_iff]
NPowProp.pow_le_mono_l [in pow_le_mono_l]
NPowProp.pow_gt_lin_r [in pow_gt_lin_r]
NPowProp.pow_1_l [in pow_1_l]
NPowProp.pow_0_l [in pow_0_l]
NPowProp.pow_mul_r [in pow_mul_r]
NPowProp.pow_add_r [in pow_add_r]
NPowProp.pow_lt_mono_r_iff [in pow_lt_mono_r_iff]
NPowProp.pow_lt_mono_l_iff [in pow_lt_mono_l_iff]
NPowProp.pow_eq_0_iff [in pow_eq_0_iff]
NPowProp.pow_add_upper [in pow_add_upper]
NPowProp.pow_le_mono [in pow_le_mono]
NPowProp.pow_eq_0 [in pow_eq_0]
NPowProp.pow_add_lower [in pow_add_lower]
NPowProp.pow_gt_1 [in pow_gt_1]
NPowProp.pow_mul_l [in pow_mul_l]
NPowProp.pow_inj_r [in pow_inj_r]
NPowProp.pow_succ_r' [in pow_succ_r']
NPowProp.pow_lt_mono_r [in pow_lt_mono_r]
Nsame_bit0 [in Nsame_bit0]
Nshiftl_nat_S [in Nshiftl_nat_S]
nshiftl_n_0 [in nshiftl_n_0]
Nshiftl_nat_spec_low [in Nshiftl_nat_spec_low]
nshiftl_size [in nshiftl_size]
nshiftl_above_size [in nshiftl_above_size]
Nshiftl_nat_equiv [in Nshiftl_nat_equiv]
Nshiftl_nat_spec_high [in Nshiftl_nat_spec_high]
nshiftl_S_tail [in nshiftl_S_tail]
nshiftl_S [in nshiftl_S]
Nshiftl_equiv_nat [in Nshiftl_equiv_nat]
nshiftr_S_tail [in nshiftr_S_tail]
nshiftr_n_0 [in nshiftr_n_0]
Nshiftr_equiv_nat [in Nshiftr_equiv_nat]
Nshiftr_nat_equiv [in Nshiftr_nat_equiv]
nshiftr_S [in nshiftr_S]
nshiftr_predsize_0_firstl [in nshiftr_predsize_0_firstl]
Nshiftr_nat_spec [in Nshiftr_nat_spec]
Nshiftr_nat_S [in Nshiftr_nat_S]
nshiftr_size [in nshiftr_size]
nshiftr_above_size [in nshiftr_above_size]
nshiftr_0_propagates [in nshiftr_0_propagates]
nshiftr_0_firstl [in nshiftr_0_firstl]
NSqrtProp.add_sqrt_le [in add_sqrt_le]
NSqrtProp.sqrt_le_lin [in sqrt_le_lin]
NSqrtProp.sqrt_succ_le [in sqrt_succ_le]
NSqrtProp.sqrt_le_square [in sqrt_le_square]
NSqrtProp.sqrt_succ_or [in sqrt_succ_or]
NSqrtProp.sqrt_lt_square [in sqrt_lt_square]
NSqrtProp.sqrt_spec' [in sqrt_spec']
NSqrtProp.sqrt_mul_above [in sqrt_mul_above]
NSqrtProp.sqrt_square [in sqrt_square]
NStrongRecProp.strong_rec_0 [in strong_rec_0]
NStrongRecProp.strong_rec_alt [in strong_rec_alt]
NStrongRecProp.strong_rec0_succ [in strong_rec0_succ]
NStrongRecProp.strong_rec0_0 [in strong_rec0_0]
NStrongRecProp.strong_rec0_more_steps [in strong_rec0_more_steps]
NStrongRecProp.strong_rec_fixpoint [in strong_rec_fixpoint]
NStrongRecProp.strong_rec0_fixpoint [in strong_rec0_fixpoint]
NStrongRecProp.strong_rec_0_any [in strong_rec_0_any]
NStrongRecProp.strong_rec_any_fst_arg [in strong_rec_any_fst_arg]
NSubProp.add_sub_assoc [in add_sub_assoc]
NSubProp.add_dichotomy [in add_dichotomy]
NSubProp.add_sub_swap [in add_sub_swap]
NSubProp.add_sub_eq_nz [in add_sub_eq_nz]
NSubProp.add_sub_eq_l [in add_sub_eq_l]
NSubProp.add_sub [in add_sub]
NSubProp.add_sub_eq_r [in add_sub_eq_r]
NSubProp.le_add_le_sub_r [in le_add_le_sub_r]
NSubProp.le_equiv [in le_equiv]
NSubProp.le_sub_le_add_l [in le_sub_le_add_l]
NSubProp.le_sub_l [in le_sub_l]
NSubProp.le_sub_le_add_r [in le_sub_le_add_r]
NSubProp.le_add_le_sub_l [in le_add_le_sub_l]
NSubProp.le_alt_dichotomy [in le_alt_dichotomy]
NSubProp.lt_sub_lt_add_r [in lt_sub_lt_add_r]
NSubProp.lt_equiv [in lt_equiv]
NSubProp.lt_add_lt_sub_r [in lt_add_lt_sub_r]
NSubProp.lt_add_lt_sub_l [in lt_add_lt_sub_l]
NSubProp.lt_sub_lt_add_l [in lt_sub_lt_add_l]
NSubProp.mul_sub_distr_r [in mul_sub_distr_r]
NSubProp.mul_pred_r [in mul_pred_r]
NSubProp.mul_sub_distr_l [in mul_sub_distr_l]
NSubProp.sub_le_mono_l [in sub_le_mono_l]
NSubProp.sub_gt [in sub_gt]
NSubProp.sub_0_l [in sub_0_l]
NSubProp.sub_le_mono_r [in sub_le_mono_r]
NSubProp.sub_succ_l [in sub_succ_l]
NSubProp.sub_0_le [in sub_0_le]
NSubProp.sub_add [in sub_add]
NSubProp.sub_succ [in sub_succ]
NSubProp.sub_diag [in sub_diag]
NSubProp.sub_add_le [in sub_add_le]
NSubProp.sub_lt [in sub_lt]
NSubProp.sub_add_distr [in sub_add_distr]
Ntestbit_Nbit [in Ntestbit_Nbit]
ntheq_eqst [in ntheq_eqst]
nth_indep [in nth_indep]
nth_In [in nth_In]
nth_S_cons [in nth_S_cons]
nth_map [in nth_map]
nth_default_eq [in nth_default_eq]
nth_order_last [in nth_order_last]
nth_map2 [in nth_map2]
nth_le [in nth_le]
nth_in_or_default [in nth_in_or_default]
nth_overflow [in nth_overflow]
NTypeIsNAxioms.add_succ_l [in add_succ_l]
NTypeIsNAxioms.add_0_l [in add_0_l]
NTypeIsNAxioms.bi_induction [in bi_induction]
NTypeIsNAxioms.BS [in BS]
NTypeIsNAxioms.B_holds [in B_holds]
NTypeIsNAxioms.B0 [in B0]
NTypeIsNAxioms.compare_lt_iff [in compare_lt_iff]
NTypeIsNAxioms.compare_antisym [in compare_antisym]
NTypeIsNAxioms.compare_le_iff [in compare_le_iff]
NTypeIsNAxioms.compare_eq_iff [in compare_eq_iff]
NTypeIsNAxioms.div_mod [in div_mod]
NTypeIsNAxioms.div2_spec [in div2_spec]
NTypeIsNAxioms.eqb_eq [in eqb_eq]
NTypeIsNAxioms.even_spec [in even_spec]
NTypeIsNAxioms.gcd_nonneg [in gcd_nonneg]
NTypeIsNAxioms.gcd_greatest [in gcd_greatest]
NTypeIsNAxioms.gcd_divide_r [in gcd_divide_r]
NTypeIsNAxioms.gcd_divide_l [in gcd_divide_l]
NTypeIsNAxioms.land_spec [in land_spec]
NTypeIsNAxioms.ldiff_spec [in ldiff_spec]
NTypeIsNAxioms.leb_le [in leb_le]
NTypeIsNAxioms.log2_spec [in log2_spec]
NTypeIsNAxioms.log2_nonpos [in log2_nonpos]
NTypeIsNAxioms.lor_spec [in lor_spec]
NTypeIsNAxioms.ltb_lt [in ltb_lt]
NTypeIsNAxioms.lt_succ_r [in lt_succ_r]
NTypeIsNAxioms.lxor_spec [in lxor_spec]
NTypeIsNAxioms.max_r [in max_r]
NTypeIsNAxioms.max_l [in max_l]
NTypeIsNAxioms.min_r [in min_r]
NTypeIsNAxioms.min_l [in min_l]
NTypeIsNAxioms.mod_bound_pos [in mod_bound_pos]
NTypeIsNAxioms.mul_succ_l [in mul_succ_l]
NTypeIsNAxioms.mul_0_l [in mul_0_l]
NTypeIsNAxioms.odd_spec [in odd_spec]
NTypeIsNAxioms.one_succ [in one_succ]
NTypeIsNAxioms.pow_pow_N [in pow_pow_N]
NTypeIsNAxioms.pow_0_r [in pow_0_r]
NTypeIsNAxioms.pow_pos_N [in pow_pos_N]
NTypeIsNAxioms.pow_succ_r [in pow_succ_r]
NTypeIsNAxioms.pow_N_pow [in pow_N_pow]
NTypeIsNAxioms.pow_neg_r [in pow_neg_r]
NTypeIsNAxioms.pred_succ [in pred_succ]
NTypeIsNAxioms.pred_0 [in pred_0]
NTypeIsNAxioms.recursion_0 [in recursion_0]
NTypeIsNAxioms.recursion_succ [in recursion_succ]
NTypeIsNAxioms.shiftl_spec_low [in shiftl_spec_low]
NTypeIsNAxioms.shiftl_spec_high [in shiftl_spec_high]
NTypeIsNAxioms.shiftr_spec [in shiftr_spec]
NTypeIsNAxioms.spec_divide [in spec_divide]
NTypeIsNAxioms.spec_N_of_Z [in spec_N_of_Z]
NTypeIsNAxioms.sqrt_spec [in sqrt_spec]
NTypeIsNAxioms.sqrt_neg [in sqrt_neg]
NTypeIsNAxioms.square_spec [in square_spec]
NTypeIsNAxioms.sub_succ_r [in sub_succ_r]
NTypeIsNAxioms.sub_0_r [in sub_0_r]
NTypeIsNAxioms.testbit_even_0 [in testbit_even_0]
NTypeIsNAxioms.testbit_neg_r [in testbit_neg_r]
NTypeIsNAxioms.testbit_even_succ [in testbit_even_succ]
NTypeIsNAxioms.testbit_odd_0 [in testbit_odd_0]
NTypeIsNAxioms.testbit_odd_succ [in testbit_odd_succ]
NTypeIsNAxioms.two_succ [in two_succ]
null_derivative_1 [in null_derivative_1]
null_derivative_loc [in null_derivative_loc]
null_derivative_0 [in null_derivative_0]
nu_left_inv [in nu_left_inv]
Nxor_eq_false [in Nxor_eq_false]
Nxor_semantics [in Nxor_semantics]
Nxor_bit0 [in Nxor_bit0]
Nxor_BVxor [in Nxor_BVxor]
Nxor_eq_true [in Nxor_eq_true]
Nxor_div2 [in Nxor_div2]
NZAddOrderProp.add_lt_cases [in add_lt_cases]
NZAddOrderProp.add_nonneg_cases [in add_nonneg_cases]
NZAddOrderProp.add_pos_nonneg [in add_pos_nonneg]
NZAddOrderProp.add_le_cases [in add_le_cases]
NZAddOrderProp.add_nonpos_cases [in add_nonpos_cases]
NZAddOrderProp.add_lt_mono [in add_lt_mono]
NZAddOrderProp.add_le_mono_r [in add_le_mono_r]
NZAddOrderProp.add_lt_le_mono [in add_lt_le_mono]
NZAddOrderProp.add_nonneg_nonneg [in add_nonneg_nonneg]
NZAddOrderProp.add_neg_cases [in add_neg_cases]
NZAddOrderProp.add_pos_pos [in add_pos_pos]
NZAddOrderProp.add_nonneg_pos [in add_nonneg_pos]
NZAddOrderProp.add_lt_mono_l [in add_lt_mono_l]
NZAddOrderProp.add_le_mono_l [in add_le_mono_l]
NZAddOrderProp.add_le_lt_mono [in add_le_lt_mono]
NZAddOrderProp.add_le_mono [in add_le_mono]
NZAddOrderProp.add_pos_cases [in add_pos_cases]
NZAddOrderProp.add_lt_mono_r [in add_lt_mono_r]
NZAddOrderProp.le_lt_add_lt [in le_lt_add_lt]
NZAddOrderProp.le_le_add_le [in le_le_add_le]
NZAddOrderProp.le_exists_sub [in le_exists_sub]
NZAddOrderProp.lt_add_pos_l [in lt_add_pos_l]
NZAddOrderProp.lt_le_add_lt [in lt_le_add_lt]
NZAddOrderProp.lt_add_pos_r [in lt_add_pos_r]
NZAddProp.add_1_r [in add_1_r]
NZAddProp.add_shuffle0 [in add_shuffle0]
NZAddProp.add_succ_r [in add_succ_r]
NZAddProp.add_cancel_l [in add_cancel_l]
NZAddProp.add_0_r [in add_0_r]
NZAddProp.add_assoc [in add_assoc]
NZAddProp.add_comm [in add_comm]
NZAddProp.add_shuffle2 [in add_shuffle2]
NZAddProp.add_shuffle3 [in add_shuffle3]
NZAddProp.add_1_l [in add_1_l]
NZAddProp.add_cancel_r [in add_cancel_r]
NZAddProp.add_succ_comm [in add_succ_comm]
NZAddProp.add_shuffle1 [in add_shuffle1]
NZAddProp.sub_1_r [in sub_1_r]
NZBaseProp.central_induction [in central_induction]
NZBaseProp.eq_sym_iff [in eq_sym_iff]
NZBaseProp.eq_stepl [in eq_stepl]
NZBaseProp.neq_sym [in neq_sym]
NZBaseProp.succ_inj [in succ_inj]
NZBaseProp.succ_inj_wd_neg [in succ_inj_wd_neg]
NZBaseProp.succ_inj_wd [in succ_inj_wd]
NZCyclicAxiomsMod.add_succ_l [in add_succ_l]
NZCyclicAxiomsMod.add_0_l [in add_0_l]
NZCyclicAxiomsMod.bi_induction [in bi_induction]
NZCyclicAxiomsMod.BS [in BS]
NZCyclicAxiomsMod.B_holds [in B_holds]
NZCyclicAxiomsMod.B0 [in B0]
NZCyclicAxiomsMod.gt_wB_1 [in gt_wB_1]
NZCyclicAxiomsMod.gt_wB_0 [in gt_wB_0]
NZCyclicAxiomsMod.mul_succ_l [in mul_succ_l]
NZCyclicAxiomsMod.mul_0_l [in mul_0_l]
NZCyclicAxiomsMod.NZ_to_Z_mod [in NZ_to_Z_mod]
NZCyclicAxiomsMod.one_mod_wB [in one_mod_wB]
NZCyclicAxiomsMod.one_succ [in one_succ]
NZCyclicAxiomsMod.pred_mod_wB [in pred_mod_wB]
NZCyclicAxiomsMod.pred_succ [in pred_succ]
NZCyclicAxiomsMod.sub_succ_r [in sub_succ_r]
NZCyclicAxiomsMod.sub_0_r [in sub_0_r]
NZCyclicAxiomsMod.succ_mod_wB [in succ_mod_wB]
NZCyclicAxiomsMod.two_succ [in two_succ]
NZDivProp.add_mod_idemp_r [in add_mod_idemp_r]
NZDivProp.add_mod_idemp_l [in add_mod_idemp_l]
NZDivProp.add_mod [in add_mod]
NZDivProp.div_mod_unique [in div_mod_unique]
NZDivProp.div_unique [in div_unique]
NZDivProp.div_small_iff [in div_small_iff]
NZDivProp.div_mul_le [in div_mul_le]
NZDivProp.div_mul [in div_mul]
NZDivProp.div_0_l [in div_0_l]
NZDivProp.div_div [in div_div]
NZDivProp.div_add [in div_add]
NZDivProp.div_1_l [in div_1_l]
NZDivProp.div_exact [in div_exact]
NZDivProp.div_le_mono [in div_le_mono]
NZDivProp.div_same [in div_same]
NZDivProp.div_pos [in div_pos]
NZDivProp.div_unique_exact [in div_unique_exact]
NZDivProp.div_mul_cancel_r [in div_mul_cancel_r]
NZDivProp.div_le_compat_l [in div_le_compat_l]
NZDivProp.div_le_upper_bound [in div_le_upper_bound]
NZDivProp.div_lt [in div_lt]
NZDivProp.div_mul_cancel_l [in div_mul_cancel_l]
NZDivProp.div_le_lower_bound [in div_le_lower_bound]
NZDivProp.div_small [in div_small]
NZDivProp.div_str_pos_iff [in div_str_pos_iff]
NZDivProp.div_str_pos [in div_str_pos]
NZDivProp.div_1_r [in div_1_r]
NZDivProp.div_lt_upper_bound [in div_lt_upper_bound]
NZDivProp.div_add_l [in div_add_l]
NZDivProp.mod_1_r [in mod_1_r]
NZDivProp.mod_small_iff [in mod_small_iff]
NZDivProp.mod_mul_r [in mod_mul_r]
NZDivProp.mod_unique [in mod_unique]
NZDivProp.mod_le [in mod_le]
NZDivProp.mod_add [in mod_add]
NZDivProp.mod_small [in mod_small]
NZDivProp.mod_mod [in mod_mod]
NZDivProp.mod_divides [in mod_divides]
NZDivProp.mod_0_l [in mod_0_l]
NZDivProp.mod_mul [in mod_mul]
NZDivProp.mod_same [in mod_same]
NZDivProp.mod_1_l [in mod_1_l]
NZDivProp.mul_succ_div_gt [in mul_succ_div_gt]
NZDivProp.mul_mod [in mul_mod]
NZDivProp.mul_mod_distr_r [in mul_mod_distr_r]
NZDivProp.mul_mod_distr_l [in mul_mod_distr_l]
NZDivProp.mul_mod_idemp_r [in mul_mod_idemp_r]
NZDivProp.mul_mod_idemp_l [in mul_mod_idemp_l]
NZDivProp.mul_div_le [in mul_div_le]
NZDomainProp.bi_induction_pred [in bi_induction_pred]
NZDomainProp.central_induction_pred [in central_induction_pred]
NZDomainProp.initial_unique [in initial_unique]
NZDomainProp.initial_alt [in initial_alt]
NZDomainProp.initial_alt2 [in initial_alt2]
NZDomainProp.initial_ancestor [in initial_ancestor]
NZDomainProp.itersucc_or_iterpred [in itersucc_or_iterpred]
NZDomainProp.itersucc_or_itersucc [in itersucc_or_itersucc]
NZDomainProp.itersucc0_or_iterpred0 [in itersucc0_or_iterpred0]
NZDomainProp.succ_onto_gives_succ_pred [in succ_onto_gives_succ_pred]
NZDomainProp.succ_swap_pred [in succ_swap_pred]
NZDomainProp.succ_onto_pred_injective [in succ_onto_pred_injective]
NZDomainProp.succ_pred_approx [in succ_pred_approx]
NZGcdProp.divide_0_r [in divide_0_r]
NZGcdProp.divide_pos_le [in divide_pos_le]
NZGcdProp.divide_factor_r [in divide_factor_r]
NZGcdProp.divide_refl [in divide_refl]
NZGcdProp.divide_factor_l [in divide_factor_l]
NZGcdProp.divide_gcd_iff [in divide_gcd_iff]
NZGcdProp.divide_1_r_nonneg [in divide_1_r_nonneg]
NZGcdProp.divide_mul_l [in divide_mul_l]
NZGcdProp.divide_antisym_nonneg [in divide_antisym_nonneg]
NZGcdProp.divide_1_l [in divide_1_l]
NZGcdProp.divide_add_r [in divide_add_r]
NZGcdProp.divide_trans [in divide_trans]
NZGcdProp.divide_mul_r [in divide_mul_r]
NZGcdProp.divide_0_l [in divide_0_l]
NZGcdProp.eq_mul_1_nonneg [in eq_mul_1_nonneg]
NZGcdProp.eq_mul_1_nonneg' [in eq_mul_1_nonneg']
NZGcdProp.gcd_diag_nonneg [in gcd_diag_nonneg]
NZGcdProp.gcd_0_l_nonneg [in gcd_0_l_nonneg]
NZGcdProp.gcd_0_r_nonneg [in gcd_0_r_nonneg]
NZGcdProp.gcd_comm [in gcd_comm]
NZGcdProp.gcd_eq_0_l [in gcd_eq_0_l]
NZGcdProp.gcd_eq_0 [in gcd_eq_0]
NZGcdProp.gcd_eq_0_r [in gcd_eq_0_r]
NZGcdProp.gcd_divide_iff [in gcd_divide_iff]
NZGcdProp.gcd_1_r [in gcd_1_r]
NZGcdProp.gcd_unique_alt [in gcd_unique_alt]
NZGcdProp.gcd_unique [in gcd_unique]
NZGcdProp.gcd_assoc [in gcd_assoc]
NZGcdProp.gcd_mul_diag_l [in gcd_mul_diag_l]
NZGcdProp.gcd_1_l [in gcd_1_l]
NZGcdProp.mul_divide_mono_r [in mul_divide_mono_r]
NZGcdProp.mul_divide_mono_l [in mul_divide_mono_l]
NZGcdProp.mul_divide_cancel_r [in mul_divide_cancel_r]
NZGcdProp.mul_divide_cancel_l [in mul_divide_cancel_l]
NZLog2Prop.add_log2_lt [in add_log2_lt]
NZLog2Prop.log2_le_mono [in log2_le_mono]
NZLog2Prop.log2_pos [in log2_pos]
NZLog2Prop.log2_eq_succ_iff_pow2 [in log2_eq_succ_iff_pow2]
NZLog2Prop.log2_succ_double [in log2_succ_double]
NZLog2Prop.log2_pow2 [in log2_pow2]
NZLog2Prop.log2_eq_succ_is_pow2 [in log2_eq_succ_is_pow2]
NZLog2Prop.log2_pred_pow2 [in log2_pred_pow2]
NZLog2Prop.log2_le_lin [in log2_le_lin]
NZLog2Prop.log2_le_pow2 [in log2_le_pow2]
NZLog2Prop.log2_succ_or [in log2_succ_or]
NZLog2Prop.log2_nonneg [in log2_nonneg]
NZLog2Prop.log2_mul_pow2 [in log2_mul_pow2]
NZLog2Prop.log2_lt_pow2 [in log2_lt_pow2]
NZLog2Prop.log2_mul_above [in log2_mul_above]
NZLog2Prop.log2_succ_le [in log2_succ_le]
NZLog2Prop.log2_unique' [in log2_unique']
NZLog2Prop.log2_lt_cancel [in log2_lt_cancel]
NZLog2Prop.log2_same [in log2_same]
NZLog2Prop.log2_double [in log2_double]
NZLog2Prop.log2_null [in log2_null]
NZLog2Prop.log2_lt_lin [in log2_lt_lin]
NZLog2Prop.log2_mul_below [in log2_mul_below]
NZLog2Prop.log2_1 [in log2_1]
NZLog2Prop.log2_2 [in log2_2]
NZLog2Prop.log2_add_le [in log2_add_le]
NZLog2Prop.log2_unique [in log2_unique]
NZLog2Prop.log2_spec_alt [in log2_spec_alt]
NZLog2UpProp.add_log2_up_lt [in add_log2_up_lt]
NZLog2UpProp.le_log2_log2_up [in le_log2_log2_up]
NZLog2UpProp.le_log2_up_succ_log2 [in le_log2_up_succ_log2]
NZLog2UpProp.log2_up_null [in log2_up_null]
NZLog2UpProp.log2_up_succ_pow2 [in log2_up_succ_pow2]
NZLog2UpProp.log2_up_double [in log2_up_double]
NZLog2UpProp.log2_up_le_mono [in log2_up_le_mono]
NZLog2UpProp.log2_up_mul_pow2 [in log2_up_mul_pow2]
NZLog2UpProp.log2_up_le_pow2 [in log2_up_le_pow2]
NZLog2UpProp.log2_log2_up_exact [in log2_log2_up_exact]
NZLog2UpProp.log2_up_same [in log2_up_same]
NZLog2UpProp.log2_up_succ_or [in log2_up_succ_or]
NZLog2UpProp.log2_up_lt_cancel [in log2_up_lt_cancel]
NZLog2UpProp.log2_up_pos [in log2_up_pos]
NZLog2UpProp.log2_up_mul_above [in log2_up_mul_above]
NZLog2UpProp.log2_up_lt_pow2 [in log2_up_lt_pow2]
NZLog2UpProp.log2_up_pow2 [in log2_up_pow2]
NZLog2UpProp.log2_up_eqn [in log2_up_eqn]
NZLog2UpProp.log2_up_1 [in log2_up_1]
NZLog2UpProp.log2_log2_up_spec [in log2_log2_up_spec]
NZLog2UpProp.log2_up_succ_double [in log2_up_succ_double]
NZLog2UpProp.log2_up_eq_succ_iff_pow2 [in log2_up_eq_succ_iff_pow2]
NZLog2UpProp.log2_up_nonneg [in log2_up_nonneg]
NZLog2UpProp.log2_up_2 [in log2_up_2]
NZLog2UpProp.log2_up_spec [in log2_up_spec]
NZLog2UpProp.log2_up_unique [in log2_up_unique]
NZLog2UpProp.log2_up_add_le [in log2_up_add_le]
NZLog2UpProp.log2_up_mul_below [in log2_up_mul_below]
NZLog2UpProp.log2_up_le_lin [in log2_up_le_lin]
NZLog2UpProp.log2_up_succ_le [in log2_up_succ_le]
NZLog2UpProp.log2_up_nonpos [in log2_up_nonpos]
NZLog2UpProp.log2_up_eq_succ_is_pow2 [in log2_up_eq_succ_is_pow2]
NZLog2UpProp.log2_up_lt_lin [in log2_up_lt_lin]
NZLog2UpProp.log2_up_eqn0 [in log2_up_eqn0]
NZMulOrderProp.add_square_le [in add_square_le]
NZMulOrderProp.add_le_mul [in add_le_mul]
NZMulOrderProp.crossmul_le_addsquare [in crossmul_le_addsquare]
NZMulOrderProp.eq_mul_0_r [in eq_mul_0_r]
NZMulOrderProp.eq_mul_0 [in eq_mul_0]
NZMulOrderProp.eq_mul_0_l [in eq_mul_0_l]
NZMulOrderProp.eq_square_0 [in eq_square_0]
NZMulOrderProp.lt_0_mul [in lt_0_mul]
NZMulOrderProp.lt_1_mul_pos [in lt_1_mul_pos]
NZMulOrderProp.mul_le_mono_nonpos_l [in mul_le_mono_nonpos_l]
NZMulOrderProp.mul_le_mono_pos_r [in mul_le_mono_pos_r]
NZMulOrderProp.mul_le_mono_neg_l [in mul_le_mono_neg_l]
NZMulOrderProp.mul_le_mono_pos_l [in mul_le_mono_pos_l]
NZMulOrderProp.mul_lt_mono_neg_r [in mul_lt_mono_neg_r]
NZMulOrderProp.mul_le_mono_nonneg_r [in mul_le_mono_nonneg_r]
NZMulOrderProp.mul_lt_mono_nonneg [in mul_lt_mono_nonneg]
NZMulOrderProp.mul_lt_pred [in mul_lt_pred]
NZMulOrderProp.mul_lt_mono_pos_r [in mul_lt_mono_pos_r]
NZMulOrderProp.mul_pos_cancel_l [in mul_pos_cancel_l]
NZMulOrderProp.mul_pos_pos [in mul_pos_pos]
NZMulOrderProp.mul_2_mono_l [in mul_2_mono_l]
NZMulOrderProp.mul_cancel_l [in mul_cancel_l]
NZMulOrderProp.mul_cancel_r [in mul_cancel_r]
NZMulOrderProp.mul_le_mono_neg_r [in mul_le_mono_neg_r]
NZMulOrderProp.mul_lt_mono_neg_l [in mul_lt_mono_neg_l]
NZMulOrderProp.mul_le_mono_nonneg_l [in mul_le_mono_nonneg_l]
NZMulOrderProp.mul_le_mono_nonneg [in mul_le_mono_nonneg]
NZMulOrderProp.mul_le_mono_nonpos_r [in mul_le_mono_nonpos_r]
NZMulOrderProp.mul_lt_mono_pos_l [in mul_lt_mono_pos_l]
NZMulOrderProp.mul_pos_cancel_r [in mul_pos_cancel_r]
NZMulOrderProp.mul_neg_neg [in mul_neg_neg]
NZMulOrderProp.mul_pos_neg [in mul_pos_neg]
NZMulOrderProp.mul_nonneg_nonneg [in mul_nonneg_nonneg]
NZMulOrderProp.mul_neg_pos [in mul_neg_pos]
NZMulOrderProp.mul_id_r [in mul_id_r]
NZMulOrderProp.mul_id_l [in mul_id_l]
NZMulOrderProp.mul_nonneg_cancel_l [in mul_nonneg_cancel_l]
NZMulOrderProp.mul_nonneg_cancel_r [in mul_nonneg_cancel_r]
NZMulOrderProp.neq_mul_0 [in neq_mul_0]
NZMulOrderProp.quadmul_le_squareadd [in quadmul_le_squareadd]
NZMulOrderProp.square_le_simpl_nonneg [in square_le_simpl_nonneg]
NZMulOrderProp.square_lt_mono_nonneg [in square_lt_mono_nonneg]
NZMulOrderProp.square_lt_simpl_nonneg [in square_lt_simpl_nonneg]
NZMulOrderProp.square_le_mono_nonneg [in square_le_mono_nonneg]
NZMulOrderProp.square_nonneg [in square_nonneg]
NZMulOrderProp.square_add_le [in square_add_le]
NZMulProp.mul_shuffle1 [in mul_shuffle1]
NZMulProp.mul_shuffle3 [in mul_shuffle3]
NZMulProp.mul_1_r [in mul_1_r]
NZMulProp.mul_add_distr_l [in mul_add_distr_l]
NZMulProp.mul_1_l [in mul_1_l]
NZMulProp.mul_succ_r [in mul_succ_r]
NZMulProp.mul_add_distr_r [in mul_add_distr_r]
NZMulProp.mul_shuffle2 [in mul_shuffle2]
NZMulProp.mul_0_r [in mul_0_r]
NZMulProp.mul_comm [in mul_comm]
NZMulProp.mul_assoc [in mul_assoc]
NZMulProp.mul_shuffle0 [in mul_shuffle0]
NZOfNatOps.ofnat_sub_r [in ofnat_sub_r]
NZOfNatOps.ofnat_sub [in ofnat_sub]
NZOfNatOps.ofnat_mul [in ofnat_mul]
NZOfNatOps.ofnat_add [in ofnat_add]
NZOfNatOps.ofnat_add_l [in ofnat_add_l]
NZOfNatOrd.ofnat_eq [in ofnat_eq]
NZOfNatOrd.ofnat_S_neq_0 [in ofnat_S_neq_0]
NZOfNatOrd.ofnat_lt [in ofnat_lt]
NZOfNatOrd.ofnat_le [in ofnat_le]
NZOfNatOrd.ofnat_injective [in ofnat_injective]
NZOfNatOrd.ofnat_S_gt_0 [in ofnat_S_gt_0]
NZOfNat.ofnat_succ [in ofnat_succ]
NZOfNat.ofnat_zero [in ofnat_zero]
NZOfNat.ofnat_pred [in ofnat_pred]
NZOrderProp.A'A_right [in A'A_right]
NZOrderProp.A'A_left [in A'A_left]
NZOrderProp.eq_dne [in eq_dne]
NZOrderProp.eq_decidable [in eq_decidable]
NZOrderProp.eq_le_incl [in eq_le_incl]
NZOrderProp.gt_wf [in gt_wf]
NZOrderProp.lbase [in lbase]
NZOrderProp.left_induction' [in left_induction']
NZOrderProp.left_induction [in left_induction]
NZOrderProp.le_stepr [in le_stepr]
NZOrderProp.le_ind [in le_ind]
NZOrderProp.le_trans [in le_trans]
NZOrderProp.le_ngt [in le_ngt]
NZOrderProp.le_dne [in le_dne]
NZOrderProp.le_neq [in le_neq]
NZOrderProp.le_succ_diag_r [in le_succ_diag_r]
NZOrderProp.le_succ_r [in le_succ_r]
NZOrderProp.le_gt_cases [in le_gt_cases]
NZOrderProp.le_decidable [in le_decidable]
NZOrderProp.le_0_2 [in le_0_2]
NZOrderProp.le_stepl [in le_stepl]
NZOrderProp.le_antisymm [in le_antisymm]
NZOrderProp.le_0_1 [in le_0_1]
NZOrderProp.le_le_succ_r [in le_le_succ_r]
NZOrderProp.le_succ_l [in le_succ_l]
NZOrderProp.le_lt_trans [in le_lt_trans]
NZOrderProp.le_refl [in le_refl]
NZOrderProp.le_ge_cases [in le_ge_cases]
NZOrderProp.ls_ls' [in ls_ls']
NZOrderProp.ls'_ls'' [in ls'_ls'']
NZOrderProp.lt_lt_succ_r [in lt_lt_succ_r]
NZOrderProp.lt_asymm [in lt_asymm]
NZOrderProp.lt_le_incl [in lt_le_incl]
NZOrderProp.lt_exists_pred_strong [in lt_exists_pred_strong]
NZOrderProp.lt_gt_cases [in lt_gt_cases]
NZOrderProp.lt_stepr [in lt_stepr]
NZOrderProp.lt_ind [in lt_ind]
NZOrderProp.lt_stepl [in lt_stepl]
NZOrderProp.lt_succ_l [in lt_succ_l]
NZOrderProp.lt_nge [in lt_nge]
NZOrderProp.lt_0_2 [in lt_0_2]
NZOrderProp.lt_le_trans [in lt_le_trans]
NZOrderProp.lt_exists_pred [in lt_exists_pred]
NZOrderProp.lt_wf [in lt_wf]
NZOrderProp.lt_dne [in lt_dne]
NZOrderProp.lt_0_1 [in lt_0_1]
NZOrderProp.lt_succ_pred [in lt_succ_pred]
NZOrderProp.lt_decidable [in lt_decidable]
NZOrderProp.lt_1_2 [in lt_1_2]
NZOrderProp.lt_trans [in lt_trans]
NZOrderProp.lt_succ_diag_r [in lt_succ_diag_r]
NZOrderProp.lt_1_l [in lt_1_l]
NZOrderProp.lt_neq [in lt_neq]
NZOrderProp.lt_ge_cases [in lt_ge_cases]
NZOrderProp.lt_trichotomy [in lt_trichotomy]
NZOrderProp.neq_succ_diag_r [in neq_succ_diag_r]
NZOrderProp.neq_succ_diag_l [in neq_succ_diag_l]
NZOrderProp.nle_gt [in nle_gt]
NZOrderProp.nle_succ_diag_l [in nle_succ_diag_l]
NZOrderProp.nlt_ge [in nlt_ge]
NZOrderProp.nlt_succ_r [in nlt_succ_r]
NZOrderProp.nlt_succ_diag_l [in nlt_succ_diag_l]
NZOrderProp.order_induction' [in order_induction']
NZOrderProp.order_induction [in order_induction]
NZOrderProp.order_induction'_0 [in order_induction'_0]
NZOrderProp.order_induction_0 [in order_induction_0]
NZOrderProp.rbase [in rbase]
NZOrderProp.right_induction' [in right_induction']
NZOrderProp.right_induction [in right_induction]
NZOrderProp.rs_rs' [in rs_rs']
NZOrderProp.rs'_rs'' [in rs'_rs'']
NZOrderProp.strong_right_induction [in strong_right_induction]
NZOrderProp.strong_left_induction' [in strong_left_induction']
NZOrderProp.strong_left_induction [in strong_left_induction]
NZOrderProp.strong_right_induction' [in strong_right_induction']
NZOrderProp.succ_lt_mono [in succ_lt_mono]
NZOrderProp.succ_le_mono [in succ_le_mono]
Nzorn [in Nzorn]
NZParityProp.double_above [in double_above]
NZParityProp.double_below [in double_below]
NZParityProp.even_0 [in even_0]
NZParityProp.Even_Odd_False [in Even_Odd_False]
NZParityProp.even_add [in even_add]
NZParityProp.even_mul [in even_mul]
NZParityProp.even_succ_succ [in even_succ_succ]
NZParityProp.even_2 [in even_2]
NZParityProp.even_add_mul_2 [in even_add_mul_2]
NZParityProp.even_add_even [in even_add_even]
NZParityProp.even_1 [in even_1]
NZParityProp.Even_succ_succ [in Even_succ_succ]
NZParityProp.Even_or_Odd [in Even_or_Odd]
NZParityProp.even_succ [in even_succ]
NZParityProp.even_add_mul_even [in even_add_mul_even]
NZParityProp.Even_succ [in Even_succ]
NZParityProp.negb_odd [in negb_odd]
NZParityProp.negb_even [in negb_even]
NZParityProp.odd_mul [in odd_mul]
NZParityProp.odd_add_mul_2 [in odd_add_mul_2]
NZParityProp.odd_add_even [in odd_add_even]
NZParityProp.odd_2 [in odd_2]
NZParityProp.odd_succ [in odd_succ]
NZParityProp.odd_add [in odd_add]
NZParityProp.Odd_succ [in Odd_succ]
NZParityProp.Odd_succ_succ [in Odd_succ_succ]
NZParityProp.odd_1 [in odd_1]
NZParityProp.odd_succ_succ [in odd_succ_succ]
NZParityProp.odd_0 [in odd_0]
NZParityProp.odd_add_mul_even [in odd_add_mul_even]
NZParityProp.orb_even_odd [in orb_even_odd]
NZPowProp.pow_0_l' [in pow_0_l']
NZPowProp.pow_le_mono_r [in pow_le_mono_r]
NZPowProp.pow_inj_l [in pow_inj_l]
NZPowProp.pow_nonneg [in pow_nonneg]
NZPowProp.pow_lt_mono [in pow_lt_mono]
NZPowProp.pow_le_mono_l_iff [in pow_le_mono_l_iff]
NZPowProp.pow_nonzero [in pow_nonzero]
NZPowProp.pow_lt_mono_l [in pow_lt_mono_l]
NZPowProp.pow_le_mono_r_iff [in pow_le_mono_r_iff]
NZPowProp.pow_le_mono_l [in pow_le_mono_l]
NZPowProp.pow_gt_lin_r [in pow_gt_lin_r]
NZPowProp.pow_1_l [in pow_1_l]
NZPowProp.pow_0_l [in pow_0_l]
NZPowProp.pow_mul_r [in pow_mul_r]
NZPowProp.pow_add_r [in pow_add_r]
NZPowProp.pow_1_r [in pow_1_r]
NZPowProp.pow_lt_mono_r_iff [in pow_lt_mono_r_iff]
NZPowProp.pow_2_r [in pow_2_r]
NZPowProp.pow_lt_mono_l_iff [in pow_lt_mono_l_iff]
NZPowProp.pow_eq_0_iff [in pow_eq_0_iff]
NZPowProp.pow_add_upper [in pow_add_upper]
NZPowProp.pow_le_mono [in pow_le_mono]
NZPowProp.pow_eq_0 [in pow_eq_0]
NZPowProp.pow_pos_nonneg [in pow_pos_nonneg]
NZPowProp.pow_add_lower [in pow_add_lower]
NZPowProp.pow_gt_1 [in pow_gt_1]
NZPowProp.pow_mul_l [in pow_mul_l]
NZPowProp.pow_inj_r [in pow_inj_r]
NZPowProp.pow_lt_mono_r [in pow_lt_mono_r]
NZSqrtProp.add_sqrt_le [in add_sqrt_le]
NZSqrtProp.sqrt_unique [in sqrt_unique]
NZSqrtProp.sqrt_le_mono [in sqrt_le_mono]
NZSqrtProp.sqrt_mul_below [in sqrt_mul_below]
NZSqrtProp.sqrt_le_lin [in sqrt_le_lin]
NZSqrtProp.sqrt_1 [in sqrt_1]
NZSqrtProp.sqrt_0 [in sqrt_0]
NZSqrtProp.sqrt_lt_cancel [in sqrt_lt_cancel]
NZSqrtProp.sqrt_succ_le [in sqrt_succ_le]
NZSqrtProp.sqrt_eq_succ_iff_square [in sqrt_eq_succ_iff_square]
NZSqrtProp.sqrt_le_square [in sqrt_le_square]
NZSqrtProp.sqrt_spec_alt [in sqrt_spec_alt]
NZSqrtProp.sqrt_unique' [in sqrt_unique']
NZSqrtProp.sqrt_succ_or [in sqrt_succ_or]
NZSqrtProp.sqrt_add_le [in sqrt_add_le]
NZSqrtProp.sqrt_2 [in sqrt_2]
NZSqrtProp.sqrt_nonneg [in sqrt_nonneg]
NZSqrtProp.sqrt_lt_square [in sqrt_lt_square]
NZSqrtProp.sqrt_lt_lin [in sqrt_lt_lin]
NZSqrtProp.sqrt_spec_nonneg [in sqrt_spec_nonneg]
NZSqrtProp.sqrt_mul_above [in sqrt_mul_above]
NZSqrtProp.sqrt_square [in sqrt_square]
NZSqrtProp.sqrt_pos [in sqrt_pos]
NZSqrtProp.sqrt_pred_square [in sqrt_pred_square]
NZSqrtUpProp.add_sqrt_up_le [in add_sqrt_up_le]
NZSqrtUpProp.le_sqrt_sqrt_up [in le_sqrt_sqrt_up]
NZSqrtUpProp.le_sqrt_up_succ_sqrt [in le_sqrt_up_succ_sqrt]
NZSqrtUpProp.sqrt_up_mul_above [in sqrt_up_mul_above]
NZSqrtUpProp.sqrt_up_spec [in sqrt_up_spec]
NZSqrtUpProp.sqrt_up_1 [in sqrt_up_1]
NZSqrtUpProp.sqrt_up_le_square [in sqrt_up_le_square]
NZSqrtUpProp.sqrt_up_nonneg [in sqrt_up_nonneg]
NZSqrtUpProp.sqrt_up_eqn [in sqrt_up_eqn]
NZSqrtUpProp.sqrt_up_0 [in sqrt_up_0]
NZSqrtUpProp.sqrt_up_mul_below [in sqrt_up_mul_below]
NZSqrtUpProp.sqrt_up_eqn0 [in sqrt_up_eqn0]
NZSqrtUpProp.sqrt_sqrt_up_spec [in sqrt_sqrt_up_spec]
NZSqrtUpProp.sqrt_up_unique [in sqrt_up_unique]
NZSqrtUpProp.sqrt_up_lt_square [in sqrt_up_lt_square]
NZSqrtUpProp.sqrt_up_succ_or [in sqrt_up_succ_or]
NZSqrtUpProp.sqrt_up_succ_le [in sqrt_up_succ_le]
NZSqrtUpProp.sqrt_up_2 [in sqrt_up_2]
NZSqrtUpProp.sqrt_up_add_le [in sqrt_up_add_le]
NZSqrtUpProp.sqrt_up_eq_succ_iff_square [in sqrt_up_eq_succ_iff_square]
NZSqrtUpProp.sqrt_sqrt_up_exact [in sqrt_sqrt_up_exact]
NZSqrtUpProp.sqrt_up_pos [in sqrt_up_pos]
NZSqrtUpProp.sqrt_up_succ_square [in sqrt_up_succ_square]
NZSqrtUpProp.sqrt_up_lt_cancel [in sqrt_up_lt_cancel]
NZSqrtUpProp.sqrt_up_le_lin [in sqrt_up_le_lin]
NZSqrtUpProp.sqrt_up_le_mono [in sqrt_up_le_mono]
NZSqrtUpProp.sqrt_up_square [in sqrt_up_square]
NZSqrtUpProp.sqrt_up_lt_lin [in sqrt_up_lt_lin]
N_nat_Z [in N_nat_Z]
n_SSSn [in n_SSSn]
n_SSn [in n_SSn]
n_SSSSn [in n_SSSSn]
N_ascii_embedding [in N_ascii_embedding]
n_Sn [in n_Sn]
N.add_succ_l [in add_succ_l]
N.add_0_l [in add_0_l]
N.bi_induction [in bi_induction]
N.compare_lt_iff [in compare_lt_iff]
N.compare_antisym [in compare_antisym]
N.compare_0_r [in compare_0_r]
N.compare_le_iff [in compare_le_iff]
N.compare_eq_iff [in compare_eq_iff]
N.div_mod' [in div_mod']
N.div_eucl_spec [in div_eucl_spec]
N.div2_double [in div2_double]
N.div2_succ_double [in div2_succ_double]
N.double_add [in double_add]
N.double_mul [in double_mul]
N.double_spec [in double_spec]
N.double_inj [in double_inj]
N.eqb_eq [in eqb_eq]
N.even_spec [in even_spec]
N.gcd_nonneg [in gcd_nonneg]
N.gcd_greatest [in gcd_greatest]
N.gcd_divide_r [in gcd_divide_r]
N.gcd_divide_l [in gcd_divide_l]
N.ge_le [in ge_le]
N.ge_le_iff [in ge_le_iff]
N.ggcd_correct_divisors [in ggcd_correct_divisors]
N.ggcd_gcd [in ggcd_gcd]
N.gt_lt [in gt_lt]
N.gt_lt_iff [in gt_lt_iff]
N.land_spec [in land_spec]
N.ldiff_spec [in ldiff_spec]
N.leb_le [in leb_le]
N.le_ge [in le_ge]
N.log2_spec [in log2_spec]
N.log2_nonpos [in log2_nonpos]
N.lor_spec [in lor_spec]
N.ltb_lt [in ltb_lt]
N.lt_succ_r [in lt_succ_r]
N.lt_gt [in lt_gt]
N.lxor_spec [in lxor_spec]
N.max_r [in max_r]
N.max_l [in max_l]
N.min_r [in min_r]
N.min_l [in min_l]
N.mod_bound_pos [in mod_bound_pos]
N.mod_lt [in mod_lt]
N.mul_succ_l [in mul_succ_l]
N.mul_0_l [in mul_0_l]
N.odd_spec [in odd_spec]
N.one_succ [in one_succ]
N.peano_rect_succ [in peano_rect_succ]
N.peano_rec_succ [in peano_rec_succ]
N.peano_rect_base [in peano_rect_base]
N.peano_rec_base [in peano_rec_base]
N.pos_pred_shiftl_low [in pos_pred_shiftl_low]
N.pos_lxor_spec [in pos_lxor_spec]
N.pos_land_spec [in pos_land_spec]
N.pos_div_eucl_remainder [in pos_div_eucl_remainder]
N.pos_ldiff_spec [in pos_ldiff_spec]
N.pos_lor_spec [in pos_lor_spec]
N.pos_pred_shiftl_high [in pos_pred_shiftl_high]
N.pos_pred_spec [in pos_pred_spec]
N.pos_div_eucl_spec [in pos_div_eucl_spec]
N.pos_pred_succ [in pos_pred_succ]
N.pow_0_r [in pow_0_r]
N.pow_succ_r [in pow_succ_r]
N.pow_neg_r [in pow_neg_r]
N.pred_div2_up [in pred_div2_up]
N.pred_sub [in pred_sub]
N.pred_succ [in pred_succ]
N.Private_BootStrap.le_0_l [in le_0_l]
N.Private_BootStrap.add_0_r [in add_0_r]
N.Private_BootStrap.add_assoc [in add_assoc]
N.Private_BootStrap.add_comm [in add_comm]
N.Private_BootStrap.sub_add [in sub_add]
N.Private_BootStrap.mul_comm [in mul_comm]
N.Private_BootStrap.add_lt_cancel_l [in add_lt_cancel_l]
N.Private_BootStrap.leb_spec [in leb_spec]
N.recursion_0 [in recursion_0]
N.recursion_succ [in recursion_succ]
N.shiftl_succ_r [in shiftl_succ_r]
N.shiftl_spec_low [in shiftl_spec_low]
N.shiftl_spec_high [in shiftl_spec_high]
N.shiftr_spec [in shiftr_spec]
N.shiftr_succ_r [in shiftr_succ_r]
N.size_gt [in size_gt]
N.size_le [in size_le]
N.size_log2 [in size_log2]
N.sqrtrem_sqrt [in sqrtrem_sqrt]
N.sqrtrem_spec [in sqrtrem_spec]
N.sqrt_spec [in sqrt_spec]
N.sqrt_neg [in sqrt_neg]
N.square_spec [in square_spec]
N.sub_succ_r [in sub_succ_r]
N.sub_0_r [in sub_0_r]
N.succ_0_discr [in succ_0_discr]
N.succ_double_inj [in succ_double_inj]
N.succ_pos_pred [in succ_pos_pred]
N.succ_double_lt [in succ_double_lt]
N.succ_double_add [in succ_double_add]
N.succ_double_spec [in succ_double_spec]
N.succ_pos_spec [in succ_pos_spec]
N.succ_double_mul [in succ_double_mul]
N.testbit_even_0 [in testbit_even_0]
N.testbit_neg_r [in testbit_neg_r]
N.testbit_even_succ [in testbit_even_succ]
N.testbit_odd_0 [in testbit_odd_0]
N.testbit_odd_succ [in testbit_odd_succ]
N.testbit_succ_r_div2 [in testbit_succ_r_div2]
N.two_succ [in two_succ]
N0_less_1 [in N0_less_1]
N0_less_2 [in N0_less_2]
N2Bv_N2Bv_gen [in N2Bv_N2Bv_gen]
N2Bv_Bv2N [in N2Bv_Bv2N]
N2Bv_N2Bv_gen_above [in N2Bv_N2Bv_gen_above]
N2Nat.id [in id]
N2Nat.inj [in inj]
N2Nat.inj_max [in inj_max]
N2Nat.inj_succ_double [in inj_succ_double]
N2Nat.inj_mul [in inj_mul]
N2Nat.inj_double [in inj_double]
N2Nat.inj_iff [in inj_iff]
N2Nat.inj_iter [in inj_iter]
N2Nat.inj_add [in inj_add]
N2Nat.inj_div2 [in inj_div2]
N2Nat.inj_compare [in inj_compare]
N2Nat.inj_sub [in inj_sub]
N2Nat.inj_min [in inj_min]
N2Nat.inj_pred [in inj_pred]
N2Nat.inj_succ [in inj_succ]
N2Z.id [in id]
N2Z.inj [in inj]
N2Z.inj_max [in inj_max]
N2Z.inj_lt [in inj_lt]
N2Z.inj_pos [in inj_pos]
N2Z.inj_mul [in inj_mul]
N2Z.inj_abs_N [in inj_abs_N]
N2Z.inj_mod [in inj_mod]
N2Z.inj_pred_max [in inj_pred_max]
N2Z.inj_iff [in inj_iff]
N2Z.inj_quot [in inj_quot]
N2Z.inj_0 [in inj_0]
N2Z.inj_add [in inj_add]
N2Z.inj_div2 [in inj_div2]
N2Z.inj_ge [in inj_ge]
N2Z.inj_compare [in inj_compare]
N2Z.inj_sub [in inj_sub]
N2Z.inj_testbit [in inj_testbit]
N2Z.inj_min [in inj_min]
N2Z.inj_quot2 [in inj_quot2]
N2Z.inj_le [in inj_le]
N2Z.inj_pred [in inj_pred]
N2Z.inj_succ [in inj_succ]
N2Z.inj_div [in inj_div]
N2Z.inj_rem [in inj_rem]
N2Z.inj_pow [in inj_pow]
N2Z.inj_sub_max [in inj_sub_max]
N2Z.inj_gt [in inj_gt]
N2Z.is_nonneg [in is_nonneg]