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)

Z (lemma)

Zabs_nat_N [in Zabs_nat_N]
Zabs_Qabs [in Zabs_Qabs]
Zabs_spec [in Zabs_spec]
Zabs_intro [in Zabs_intro]
Zabs_ind [in Zabs_ind]
Zabs_nat_lt [in Zabs_nat_lt]
Zabs_nat_le [in Zabs_nat_le]
Zabs_N_nat [in Zabs_N_nat]
Zabs2Nat.abs_nat_spec [in abs_nat_spec]
Zabs2Nat.abs_nat_nonneg [in abs_nat_nonneg]
Zabs2Nat.id [in id]
Zabs2Nat.id_abs [in id_abs]
Zabs2Nat.inj_succ_abs [in inj_succ_abs]
Zabs2Nat.inj_max [in inj_max]
Zabs2Nat.inj_lt [in inj_lt]
Zabs2Nat.inj_mul_abs [in inj_mul_abs]
Zabs2Nat.inj_pos [in inj_pos]
Zabs2Nat.inj_mul [in inj_mul]
Zabs2Nat.inj_0 [in inj_0]
Zabs2Nat.inj_add [in inj_add]
Zabs2Nat.inj_compare [in inj_compare]
Zabs2Nat.inj_sub [in inj_sub]
Zabs2Nat.inj_min [in inj_min]
Zabs2Nat.inj_add_abs [in inj_add_abs]
Zabs2Nat.inj_le [in inj_le]
Zabs2Nat.inj_neg [in inj_neg]
Zabs2Nat.inj_pred [in inj_pred]
Zabs2Nat.inj_succ [in inj_succ]
Zabs2N.abs_N_nonneg [in abs_N_nonneg]
Zabs2N.abs_N_spec [in abs_N_spec]
Zabs2N.id [in id]
Zabs2N.id_abs [in id_abs]
Zabs2N.inj_succ_abs [in inj_succ_abs]
Zabs2N.inj_max [in inj_max]
Zabs2N.inj_lt [in inj_lt]
Zabs2N.inj_mul_abs [in inj_mul_abs]
Zabs2N.inj_pos [in inj_pos]
Zabs2N.inj_mul [in inj_mul]
Zabs2N.inj_quot [in inj_quot]
Zabs2N.inj_0 [in inj_0]
Zabs2N.inj_add [in inj_add]
Zabs2N.inj_compare [in inj_compare]
Zabs2N.inj_sub [in inj_sub]
Zabs2N.inj_min [in inj_min]
Zabs2N.inj_opp [in inj_opp]
Zabs2N.inj_add_abs [in inj_add_abs]
Zabs2N.inj_le [in inj_le]
Zabs2N.inj_neg [in inj_neg]
Zabs2N.inj_pred [in inj_pred]
Zabs2N.inj_succ [in inj_succ]
Zabs2N.inj_rem [in inj_rem]
Zabs2N.inj_pow [in inj_pow]
ZAddOrderProp.add_neg_nonpos [in add_neg_nonpos]
ZAddOrderProp.add_nonpos_neg [in add_nonpos_neg]
ZAddOrderProp.add_nonpos_nonpos [in add_nonpos_nonpos]
ZAddOrderProp.add_neg_neg [in add_neg_neg]
ZAddOrderProp.le_add_le_sub_r [in le_add_le_sub_r]
ZAddOrderProp.le_sub_nonneg [in le_sub_nonneg]
ZAddOrderProp.le_sub_le_add [in le_sub_le_add]
ZAddOrderProp.le_sub_le_add_l [in le_sub_le_add_l]
ZAddOrderProp.le_sub_0 [in le_sub_0]
ZAddOrderProp.le_sub_le_add_r [in le_sub_le_add_r]
ZAddOrderProp.le_lt_sub_lt [in le_lt_sub_lt]
ZAddOrderProp.le_le_sub_lt [in le_le_sub_lt]
ZAddOrderProp.le_0_sub [in le_0_sub]
ZAddOrderProp.le_add_le_sub_l [in le_add_le_sub_l]
ZAddOrderProp.lt_sub_lt_add_r [in lt_sub_lt_add_r]
ZAddOrderProp.lt_sub_pos [in lt_sub_pos]
ZAddOrderProp.lt_add_lt_sub_r [in lt_add_lt_sub_r]
ZAddOrderProp.lt_add_lt_sub_l [in lt_add_lt_sub_l]
ZAddOrderProp.lt_le_sub_lt [in lt_le_sub_lt]
ZAddOrderProp.lt_sub_lt_add [in lt_sub_lt_add]
ZAddOrderProp.lt_m1_0 [in lt_m1_0]
ZAddOrderProp.lt_sub_lt_add_l [in lt_sub_lt_add_l]
ZAddOrderProp.lt_sub_0 [in lt_sub_0]
ZAddOrderProp.lt_0_sub [in lt_0_sub]
ZAddOrderProp.opp_neg_pos [in opp_neg_pos]
ZAddOrderProp.opp_nonpos_nonneg [in opp_nonpos_nonneg]
ZAddOrderProp.opp_pos_neg [in opp_pos_neg]
ZAddOrderProp.opp_lt_mono [in opp_lt_mono]
ZAddOrderProp.opp_nonneg_nonpos [in opp_nonneg_nonpos]
ZAddOrderProp.opp_le_mono [in opp_le_mono]
ZAddOrderProp.sub_le_mono_l [in sub_le_mono_l]
ZAddOrderProp.sub_lt_mono_l [in sub_lt_mono_l]
ZAddOrderProp.sub_nonneg_cases [in sub_nonneg_cases]
ZAddOrderProp.sub_le_mono_r [in sub_le_mono_r]
ZAddOrderProp.sub_lt_mono_r [in sub_lt_mono_r]
ZAddOrderProp.sub_le_cases [in sub_le_cases]
ZAddOrderProp.sub_neg_cases [in sub_neg_cases]
ZAddOrderProp.sub_le_mono [in sub_le_mono]
ZAddOrderProp.sub_lt_mono [in sub_lt_mono]
ZAddOrderProp.sub_pos_cases [in sub_pos_cases]
ZAddOrderProp.sub_lt_cases [in sub_lt_cases]
ZAddOrderProp.sub_lt_le_mono [in sub_lt_le_mono]
ZAddOrderProp.sub_nonpos_cases [in sub_nonpos_cases]
ZAddOrderProp.sub_le_lt_mono [in sub_le_lt_mono]
ZAddOrderProp.zero_pos_neg [in zero_pos_neg]
ZAddProp.add_pred_r [in add_pred_r]
ZAddProp.add_simpl_r [in add_simpl_r]
ZAddProp.add_opp_diag_l [in add_opp_diag_l]
ZAddProp.add_sub_assoc [in add_sub_assoc]
ZAddProp.add_pred_l [in add_pred_l]
ZAddProp.add_move_l [in add_move_l]
ZAddProp.add_opp_diag_r [in add_opp_diag_r]
ZAddProp.add_move_0_l [in add_move_0_l]
ZAddProp.add_add_simpl_r_l [in add_add_simpl_r_l]
ZAddProp.add_add_simpl_l_r [in add_add_simpl_l_r]
ZAddProp.add_add_simpl_l_l [in add_add_simpl_l_l]
ZAddProp.add_sub_swap [in add_sub_swap]
ZAddProp.add_move_0_r [in add_move_0_r]
ZAddProp.add_add_simpl_r_r [in add_add_simpl_r_r]
ZAddProp.add_move_r [in add_move_r]
ZAddProp.add_simpl_l [in add_simpl_l]
ZAddProp.add_opp_r [in add_opp_r]
ZAddProp.add_opp_l [in add_opp_l]
ZAddProp.eq_opp_r [in eq_opp_r]
ZAddProp.eq_opp_l [in eq_opp_l]
ZAddProp.opp_inj_wd [in opp_inj_wd]
ZAddProp.opp_involutive [in opp_involutive]
ZAddProp.opp_sub_distr [in opp_sub_distr]
ZAddProp.opp_pred [in opp_pred]
ZAddProp.opp_inj [in opp_inj]
ZAddProp.opp_add_distr [in opp_add_distr]
ZAddProp.sub_add_simpl_r_l [in sub_add_simpl_r_l]
ZAddProp.sub_add_simpl_r_r [in sub_add_simpl_r_r]
ZAddProp.sub_sub_distr [in sub_sub_distr]
ZAddProp.sub_cancel_r [in sub_cancel_r]
ZAddProp.sub_move_0_r [in sub_move_0_r]
ZAddProp.sub_0_l [in sub_0_l]
ZAddProp.sub_move_0_l [in sub_move_0_l]
ZAddProp.sub_move_l [in sub_move_l]
ZAddProp.sub_pred_l [in sub_pred_l]
ZAddProp.sub_succ_l [in sub_succ_l]
ZAddProp.sub_simpl_r [in sub_simpl_r]
ZAddProp.sub_add [in sub_add]
ZAddProp.sub_diag [in sub_diag]
ZAddProp.sub_move_r [in sub_move_r]
ZAddProp.sub_pred_r [in sub_pred_r]
ZAddProp.sub_simpl_l [in sub_simpl_l]
ZAddProp.sub_opp_r [in sub_opp_r]
ZAddProp.sub_cancel_l [in sub_cancel_l]
ZAddProp.sub_opp_l [in sub_opp_l]
ZAddProp.sub_add_distr [in sub_add_distr]
ZBaseProp.pred_inj_wd [in pred_inj_wd]
ZBaseProp.pred_inj [in pred_inj]
ZBaseProp.succ_m1 [in succ_m1]
ZBitsProp.add_carry_bits_aux [in add_carry_bits_aux]
ZBitsProp.add_bit0 [in add_bit0]
ZBitsProp.add_bit1 [in add_bit1]
ZBitsProp.add_nocarry_mod_lt_pow2 [in add_nocarry_mod_lt_pow2]
ZBitsProp.add_b2z_double_div2 [in add_b2z_double_div2]
ZBitsProp.add_carry_div2 [in add_carry_div2]
ZBitsProp.add_nocarry_lxor [in add_nocarry_lxor]
ZBitsProp.add_lnot_diag [in add_lnot_diag]
ZBitsProp.add_b2z_double_bit0 [in add_b2z_double_bit0]
ZBitsProp.add_nocarry_lt_pow2 [in add_nocarry_lt_pow2]
ZBitsProp.add_carry_bits [in add_carry_bits]
ZBitsProp.add3_bits_div2 [in add3_bits_div2]
ZBitsProp.add3_bit0 [in add3_bit0]
ZBitsProp.are_bits [in are_bits]
ZBitsProp.bits_iff_nonneg' [in bits_iff_nonneg']
ZBitsProp.bits_above_log2 [in bits_above_log2]
ZBitsProp.bits_iff_neg' [in bits_iff_neg']
ZBitsProp.bits_iff_nonneg [in bits_iff_nonneg]
ZBitsProp.bits_0 [in bits_0]
ZBitsProp.bits_above_log2_neg [in bits_above_log2_neg]
ZBitsProp.bits_iff_neg_ex [in bits_iff_neg_ex]
ZBitsProp.bits_m1 [in bits_m1]
ZBitsProp.bits_inj_0 [in bits_inj_0]
ZBitsProp.bits_iff_neg [in bits_iff_neg]
ZBitsProp.bits_inj_iff [in bits_inj_iff]
ZBitsProp.bits_inj [in bits_inj]
ZBitsProp.bits_inj_iff' [in bits_inj_iff']
ZBitsProp.bits_inj' [in bits_inj']
ZBitsProp.bits_iff_nonneg_ex [in bits_iff_nonneg_ex]
ZBitsProp.bits_opp [in bits_opp]
ZBitsProp.bit_log2 [in bit_log2]
ZBitsProp.bit_log2_neg [in bit_log2_neg]
ZBitsProp.bit0_eqb [in bit0_eqb]
ZBitsProp.bit0_odd [in bit0_odd]
ZBitsProp.bit0_mod [in bit0_mod]
ZBitsProp.b2z_bit0 [in b2z_bit0]
ZBitsProp.b2z_inj [in b2z_inj]
ZBitsProp.b2z_div2 [in b2z_div2]
ZBitsProp.clearbit_spec' [in clearbit_spec']
ZBitsProp.clearbit_iff [in clearbit_iff]
ZBitsProp.clearbit_eq [in clearbit_eq]
ZBitsProp.clearbit_neq [in clearbit_neq]
ZBitsProp.clearbit_eqb [in clearbit_eqb]
ZBitsProp.div_pow2_bits [in div_pow2_bits]
ZBitsProp.div2_nonneg [in div2_nonneg]
ZBitsProp.div2_neg [in div2_neg]
ZBitsProp.div2_div [in div2_div]
ZBitsProp.div2_bits [in div2_bits]
ZBitsProp.div2_odd [in div2_odd]
ZBitsProp.double_bits_succ [in double_bits_succ]
ZBitsProp.double_bits [in double_bits]
ZBitsProp.exists_div2 [in exists_div2]
ZBitsProp.land_comm [in land_comm]
ZBitsProp.land_assoc [in land_assoc]
ZBitsProp.land_0_l [in land_0_l]
ZBitsProp.land_m1_l [in land_m1_l]
ZBitsProp.land_ones_low [in land_ones_low]
ZBitsProp.land_ldiff [in land_ldiff]
ZBitsProp.land_lnot_diag [in land_lnot_diag]
ZBitsProp.land_neg [in land_neg]
ZBitsProp.land_lor_distr_r [in land_lor_distr_r]
ZBitsProp.land_ones [in land_ones]
ZBitsProp.land_diag [in land_diag]
ZBitsProp.land_m1_r [in land_m1_r]
ZBitsProp.land_0_r [in land_0_r]
ZBitsProp.land_lor_distr_l [in land_lor_distr_l]
ZBitsProp.land_nonneg [in land_nonneg]
ZBitsProp.ldiff_nonneg [in ldiff_nonneg]
ZBitsProp.ldiff_neg [in ldiff_neg]
ZBitsProp.ldiff_ldiff_l [in ldiff_ldiff_l]
ZBitsProp.ldiff_ones_r_low [in ldiff_ones_r_low]
ZBitsProp.ldiff_ones_r [in ldiff_ones_r]
ZBitsProp.ldiff_ones_l_low [in ldiff_ones_l_low]
ZBitsProp.ldiff_diag [in ldiff_diag]
ZBitsProp.ldiff_le [in ldiff_le]
ZBitsProp.ldiff_0_l [in ldiff_0_l]
ZBitsProp.ldiff_m1_l [in ldiff_m1_l]
ZBitsProp.ldiff_land [in ldiff_land]
ZBitsProp.ldiff_0_r [in ldiff_0_r]
ZBitsProp.ldiff_m1_r [in ldiff_m1_r]
ZBitsProp.lnot_m1 [in lnot_m1]
ZBitsProp.lnot_shiftr [in lnot_shiftr]
ZBitsProp.lnot_lxor_l [in lnot_lxor_l]
ZBitsProp.lnot_0 [in lnot_0]
ZBitsProp.lnot_neg [in lnot_neg]
ZBitsProp.lnot_nonneg [in lnot_nonneg]
ZBitsProp.lnot_ldiff [in lnot_ldiff]
ZBitsProp.lnot_lor [in lnot_lor]
ZBitsProp.lnot_land [in lnot_land]
ZBitsProp.lnot_lxor_r [in lnot_lxor_r]
ZBitsProp.lnot_involutive [in lnot_involutive]
ZBitsProp.lnot_spec [in lnot_spec]
ZBitsProp.log2_lor [in log2_lor]
ZBitsProp.log2_shiftr [in log2_shiftr]
ZBitsProp.log2_lxor [in log2_lxor]
ZBitsProp.log2_bits_unique [in log2_bits_unique]
ZBitsProp.log2_shiftl [in log2_shiftl]
ZBitsProp.log2_land [in log2_land]
ZBitsProp.log2_shiftl' [in log2_shiftl']
ZBitsProp.lor_comm [in lor_comm]
ZBitsProp.lor_neg [in lor_neg]
ZBitsProp.lor_m1_r [in lor_m1_r]
ZBitsProp.lor_eq_0_iff [in lor_eq_0_iff]
ZBitsProp.lor_ldiff_and [in lor_ldiff_and]
ZBitsProp.lor_land_distr_r [in lor_land_distr_r]
ZBitsProp.lor_eq_0_l [in lor_eq_0_l]
ZBitsProp.lor_land_distr_l [in lor_land_distr_l]
ZBitsProp.lor_m1_l [in lor_m1_l]
ZBitsProp.lor_lnot_diag [in lor_lnot_diag]
ZBitsProp.lor_0_r [in lor_0_r]
ZBitsProp.lor_ones_low [in lor_ones_low]
ZBitsProp.lor_assoc [in lor_assoc]
ZBitsProp.lor_diag [in lor_diag]
ZBitsProp.lor_0_l [in lor_0_l]
ZBitsProp.lor_nonneg [in lor_nonneg]
ZBitsProp.lxor_m1_r [in lxor_m1_r]
ZBitsProp.lxor_lnot_lnot [in lxor_lnot_lnot]
ZBitsProp.lxor_0_r [in lxor_0_r]
ZBitsProp.lxor_0_l [in lxor_0_l]
ZBitsProp.lxor_lor [in lxor_lor]
ZBitsProp.lxor_m1_l [in lxor_m1_l]
ZBitsProp.lxor_eq_0_iff [in lxor_eq_0_iff]
ZBitsProp.lxor_comm [in lxor_comm]
ZBitsProp.lxor_nonneg [in lxor_nonneg]
ZBitsProp.lxor_assoc [in lxor_assoc]
ZBitsProp.lxor_eq [in lxor_eq]
ZBitsProp.lxor_nilpotent [in lxor_nilpotent]
ZBitsProp.mod_pow2_bits_high [in mod_pow2_bits_high]
ZBitsProp.mod_pow2_bits_low [in mod_pow2_bits_low]
ZBitsProp.mul_pow2_bits_low [in mul_pow2_bits_low]
ZBitsProp.mul_pow2_bits_add [in mul_pow2_bits_add]
ZBitsProp.mul_pow2_bits [in mul_pow2_bits]
ZBitsProp.nocarry_equiv [in nocarry_equiv]
ZBitsProp.ones_mod_pow2 [in ones_mod_pow2]
ZBitsProp.ones_div_pow2 [in ones_div_pow2]
ZBitsProp.ones_spec_iff [in ones_spec_iff]
ZBitsProp.ones_add [in ones_add]
ZBitsProp.ones_equiv [in ones_equiv]
ZBitsProp.ones_spec_low [in ones_spec_low]
ZBitsProp.ones_spec_high [in ones_spec_high]
ZBitsProp.pow_div_l [in pow_div_l]
ZBitsProp.pow_sub_r [in pow_sub_r]
ZBitsProp.pow2_bits_eqb [in pow2_bits_eqb]
ZBitsProp.pow2_bits_false [in pow2_bits_false]
ZBitsProp.pow2_bits_true [in pow2_bits_true]
ZBitsProp.setbit_neq [in setbit_neq]
ZBitsProp.setbit_eqb [in setbit_eqb]
ZBitsProp.setbit_eq [in setbit_eq]
ZBitsProp.setbit_spec' [in setbit_spec']
ZBitsProp.setbit_iff [in setbit_iff]
ZBitsProp.shiftl_spec [in shiftl_spec]
ZBitsProp.shiftl_land [in shiftl_land]
ZBitsProp.shiftl_lxor [in shiftl_lxor]
ZBitsProp.shiftl_opp_r [in shiftl_opp_r]
ZBitsProp.shiftl_div_pow2 [in shiftl_div_pow2]
ZBitsProp.shiftl_1_l [in shiftl_1_l]
ZBitsProp.shiftl_nonneg [in shiftl_nonneg]
ZBitsProp.shiftl_eq_0_iff [in shiftl_eq_0_iff]
ZBitsProp.shiftl_neg [in shiftl_neg]
ZBitsProp.shiftl_0_l [in shiftl_0_l]
ZBitsProp.shiftl_mul_pow2 [in shiftl_mul_pow2]
ZBitsProp.shiftl_ldiff [in shiftl_ldiff]
ZBitsProp.shiftl_0_r [in shiftl_0_r]
ZBitsProp.shiftl_shiftl [in shiftl_shiftl]
ZBitsProp.shiftl_spec_alt [in shiftl_spec_alt]
ZBitsProp.shiftl_lor [in shiftl_lor]
ZBitsProp.shiftr_div_pow2 [in shiftr_div_pow2]
ZBitsProp.shiftr_ldiff [in shiftr_ldiff]
ZBitsProp.shiftr_opp_r [in shiftr_opp_r]
ZBitsProp.shiftr_lxor [in shiftr_lxor]
ZBitsProp.shiftr_0_l [in shiftr_0_l]
ZBitsProp.shiftr_mul_pow2 [in shiftr_mul_pow2]
ZBitsProp.shiftr_neg [in shiftr_neg]
ZBitsProp.shiftr_shiftl_l [in shiftr_shiftl_l]
ZBitsProp.shiftr_nonneg [in shiftr_nonneg]
ZBitsProp.shiftr_eq_0 [in shiftr_eq_0]
ZBitsProp.shiftr_shiftl_r [in shiftr_shiftl_r]
ZBitsProp.shiftr_land [in shiftr_land]
ZBitsProp.shiftr_lor [in shiftr_lor]
ZBitsProp.shiftr_0_r [in shiftr_0_r]
ZBitsProp.shiftr_shiftr [in shiftr_shiftr]
ZBitsProp.shiftr_eq_0_iff [in shiftr_eq_0_iff]
ZBitsProp.sub_nocarry_ldiff [in sub_nocarry_ldiff]
ZBitsProp.testbit_0_r [in testbit_0_r]
ZBitsProp.testbit_true [in testbit_true]
ZBitsProp.testbit_eqb [in testbit_eqb]
ZBitsProp.testbit_false [in testbit_false]
ZBitsProp.testbit_unique [in testbit_unique]
ZBitsProp.testbit_spec [in testbit_spec]
ZBitsProp.testbit_spec' [in testbit_spec']
ZBitsProp.testbit_succ_r [in testbit_succ_r]
ZBitsProp.testbit_odd [in testbit_odd]
Zbounded_induction [in Zbounded_induction]
Zcase_sign [in Zcase_sign]
Zcompare_mult_compat [in Zcompare_mult_compat]
Zcompare_Lt_trans [in Zcompare_Lt_trans]
Zcompare_rec [in Zcompare_rec]
Zcompare_Gt_not_Lt [in Zcompare_Gt_not_Lt]
Zcompare_opp [in Zcompare_opp]
Zcompare_Gt_trans [in Zcompare_Gt_trans]
Zcompare_succ_compat [in Zcompare_succ_compat]
Zcompare_eq_case [in Zcompare_eq_case]
Zcompare_succ_Gt [in Zcompare_succ_Gt]
Zcompare_elim [in Zcompare_elim]
Zcompare_Gt_spec [in Zcompare_Gt_spec]
Zcompare_antisym [in Zcompare_antisym]
Zcompare_Gt_Lt_antisym [in Zcompare_Gt_Lt_antisym]
Zcompare_gt [in Zcompare_gt]
Zcompare_rect [in Zcompare_rect]
Zcompare_plus_compat [in Zcompare_plus_compat]
ZC4 [in ZC4]
Zdivide_Zgcd [in Zdivide_Zgcd]
Zdivide_Zdiv_lt_pos [in Zdivide_Zdiv_lt_pos]
Zdivide_dec [in Zdivide_dec]
Zdivide_opp_l_rev [in Zdivide_opp_l_rev]
Zdivide_Zdiv_eq_2 [in Zdivide_Zdiv_eq_2]
Zdivide_opp_r [in Zdivide_opp_r]
Zdivide_Zabs_l [in Zdivide_Zabs_l]
Zdivide_opp_l [in Zdivide_opp_l]
Zdivide_le [in Zdivide_le]
Zdivide_opp_r_rev [in Zdivide_opp_r_rev]
Zdivide_Zdiv_eq [in Zdivide_Zdiv_eq]
Zdivide_mod [in Zdivide_mod]
Zdivide_Zabs_inv_l [in Zdivide_Zabs_inv_l]
Zdivide_mod_minus [in Zdivide_mod_minus]
Zdivide_bounds [in Zdivide_bounds]
Zdivide_power_2 [in Zdivide_power_2]
ZDivProp.add_mod_idemp_r [in add_mod_idemp_r]
ZDivProp.add_mod_idemp_l [in add_mod_idemp_l]
ZDivProp.add_mod [in add_mod]
ZDivProp.div_mod_unique [in div_mod_unique]
ZDivProp.div_unique [in div_unique]
ZDivProp.div_small_iff [in div_small_iff]
ZDivProp.div_unique_neg [in div_unique_neg]
ZDivProp.div_mul_le [in div_mul_le]
ZDivProp.div_mul [in div_mul]
ZDivProp.div_0_l [in div_0_l]
ZDivProp.div_div [in div_div]
ZDivProp.div_add [in div_add]
ZDivProp.div_1_l [in div_1_l]
ZDivProp.div_opp_opp [in div_opp_opp]
ZDivProp.div_exact [in div_exact]
ZDivProp.div_le_mono [in div_le_mono]
ZDivProp.div_same [in div_same]
ZDivProp.div_pos [in div_pos]
ZDivProp.div_unique_exact [in div_unique_exact]
ZDivProp.div_mul_cancel_r [in div_mul_cancel_r]
ZDivProp.div_opp_l_nz [in div_opp_l_nz]
ZDivProp.div_le_compat_l [in div_le_compat_l]
ZDivProp.div_le_upper_bound [in div_le_upper_bound]
ZDivProp.div_lt [in div_lt]
ZDivProp.div_mul_cancel_l [in div_mul_cancel_l]
ZDivProp.div_le_lower_bound [in div_le_lower_bound]
ZDivProp.div_opp_l_z [in div_opp_l_z]
ZDivProp.div_small [in div_small]
ZDivProp.div_str_pos [in div_str_pos]
ZDivProp.div_1_r [in div_1_r]
ZDivProp.div_lt_upper_bound [in div_lt_upper_bound]
ZDivProp.div_unique_pos [in div_unique_pos]
ZDivProp.div_opp_r_nz [in div_opp_r_nz]
ZDivProp.div_opp_r_z [in div_opp_r_z]
ZDivProp.div_add_l [in div_add_l]
ZDivProp.mod_1_r [in mod_1_r]
ZDivProp.mod_small_iff [in mod_small_iff]
ZDivProp.mod_opp_r_nz [in mod_opp_r_nz]
ZDivProp.mod_opp_l_z [in mod_opp_l_z]
ZDivProp.mod_unique [in mod_unique]
ZDivProp.mod_opp_l_nz [in mod_opp_l_nz]
ZDivProp.mod_opp_r_z [in mod_opp_r_z]
ZDivProp.mod_le [in mod_le]
ZDivProp.mod_add [in mod_add]
ZDivProp.mod_small [in mod_small]
ZDivProp.mod_mod [in mod_mod]
ZDivProp.mod_sign [in mod_sign]
ZDivProp.mod_eq [in mod_eq]
ZDivProp.mod_bound_abs [in mod_bound_abs]
ZDivProp.mod_0_l [in mod_0_l]
ZDivProp.mod_opp_opp [in mod_opp_opp]
ZDivProp.mod_mul [in mod_mul]
ZDivProp.mod_sign_nz [in mod_sign_nz]
ZDivProp.mod_same [in mod_same]
ZDivProp.mod_unique_pos [in mod_unique_pos]
ZDivProp.mod_sign_mul [in mod_sign_mul]
ZDivProp.mod_unique_neg [in mod_unique_neg]
ZDivProp.mod_bound_or [in mod_bound_or]
ZDivProp.mod_1_l [in mod_1_l]
ZDivProp.mul_succ_div_gt [in mul_succ_div_gt]
ZDivProp.mul_mod [in mul_mod]
ZDivProp.mul_mod_distr_r [in mul_mod_distr_r]
ZDivProp.mul_mod_distr_l [in mul_mod_distr_l]
ZDivProp.mul_mod_idemp_r [in mul_mod_idemp_r]
ZDivProp.mul_succ_div_lt [in mul_succ_div_lt]
ZDivProp.mul_div_ge [in mul_div_ge]
ZDivProp.mul_mod_idemp_l [in mul_mod_idemp_l]
ZDivProp.mul_div_le [in mul_div_le]
ZDivProp.opp_mod_bound_or [in opp_mod_bound_or]
ZDivProp.rem_mul_r [in rem_mul_r]
Zdiv_Zdiv [in Zdiv_Zdiv]
Zdiv_gcd_zero [in Zdiv_gcd_zero]
Zdiv_lt_upper_bound [in Zdiv_lt_upper_bound]
Zdiv_shift_r [in Zdiv_shift_r]
Zdiv_eucl_exist [in Zdiv_eucl_exist]
Zdiv_rest_correct2 [in Zdiv_rest_correct2]
Zdiv_1_l [in Zdiv_1_l]
Zdiv_0_l [in Zdiv_0_l]
Zdiv_mod_unique [in Zdiv_mod_unique]
Zdiv_unique [in Zdiv_unique]
Zdiv_neg [in Zdiv_neg]
Zdiv_opp_opp [in Zdiv_opp_opp]
Zdiv_mult_le [in Zdiv_mult_le]
Zdiv_rest_ok [in Zdiv_rest_ok]
Zdiv_sgn [in Zdiv_sgn]
Zdiv_Qdiv [in Zdiv_Qdiv]
Zdiv_le_lower_bound [in Zdiv_le_lower_bound]
Zdiv_eucl_extended [in Zdiv_eucl_extended]
Zdiv_1_r [in Zdiv_1_r]
Zdiv_mult_cancel_r [in Zdiv_mult_cancel_r]
Zdiv_mult_cancel_l [in Zdiv_mult_cancel_l]
Zdiv_small [in Zdiv_small]
Zdiv_rest_correct [in Zdiv_rest_correct]
Zdiv_le_upper_bound [in Zdiv_le_upper_bound]
Zdiv_mod_unique_2 [in Zdiv_mod_unique_2]
Zdiv_unique_full [in Zdiv_unique_full]
Zdiv_le_compat_l [in Zdiv_le_compat_l]
Zdiv_rest_shiftr [in Zdiv_rest_shiftr]
Zdiv_0_r [in Zdiv_0_r]
Zdiv_rest_correct1 [in Zdiv_rest_correct1]
Zdiv2_div [in Zdiv2_div]
Zdiv2_odd_eqn [in Zdiv2_odd_eqn]
Zdiv2_two_power_nat [in Zdiv2_two_power_nat]
Zegal_left [in Zegal_left]
Zeq_bool_if [in Zeq_bool_if]
Zeq_plus_swap [in Zeq_plus_swap]
Zeq_is_eq_bool [in Zeq_is_eq_bool]
Zeq_bool_neq [in Zeq_bool_neq]
Zeq_bool_eq [in Zeq_bool_eq]
Zeq_minus [in Zeq_minus]
zerob_false_elim [in zerob_false_elim]
zerob_false_intro [in zerob_false_intro]
zerob_true_elim [in zerob_true_elim]
zerob_true_intro [in zerob_true_intro]
ZERO_le_N_digits [in ZERO_le_N_digits]
ZEuclidProp.add_mod_idemp_r [in add_mod_idemp_r]
ZEuclidProp.add_mod_idemp_l [in add_mod_idemp_l]
ZEuclidProp.add_mod [in add_mod]
ZEuclidProp.div_mod_unique [in div_mod_unique]
ZEuclidProp.div_unique [in div_unique]
ZEuclidProp.div_small_iff [in div_small_iff]
ZEuclidProp.div_mul_le [in div_mul_le]
ZEuclidProp.div_mul [in div_mul]
ZEuclidProp.div_0_l [in div_0_l]
ZEuclidProp.div_div [in div_div]
ZEuclidProp.div_add [in div_add]
ZEuclidProp.div_1_l [in div_1_l]
ZEuclidProp.div_opp_opp_z [in div_opp_opp_z]
ZEuclidProp.div_exact [in div_exact]
ZEuclidProp.div_le_mono [in div_le_mono]
ZEuclidProp.div_same [in div_same]
ZEuclidProp.div_pos [in div_pos]
ZEuclidProp.div_unique_exact [in div_unique_exact]
ZEuclidProp.div_mul_cancel_r [in div_mul_cancel_r]
ZEuclidProp.div_opp_l_nz [in div_opp_l_nz]
ZEuclidProp.div_le_compat_l [in div_le_compat_l]
ZEuclidProp.div_opp_r [in div_opp_r]
ZEuclidProp.div_le_upper_bound [in div_le_upper_bound]
ZEuclidProp.div_lt [in div_lt]
ZEuclidProp.div_mul_cancel_l [in div_mul_cancel_l]
ZEuclidProp.div_le_lower_bound [in div_le_lower_bound]
ZEuclidProp.div_opp_l_z [in div_opp_l_z]
ZEuclidProp.div_small [in div_small]
ZEuclidProp.div_str_pos [in div_str_pos]
ZEuclidProp.div_1_r [in div_1_r]
ZEuclidProp.div_lt_upper_bound [in div_lt_upper_bound]
ZEuclidProp.div_opp_opp_nz [in div_opp_opp_nz]
ZEuclidProp.div_add_l [in div_add_l]
ZEuclidProp.mod_1_r [in mod_1_r]
ZEuclidProp.mod_small_iff [in mod_small_iff]
ZEuclidProp.mod_opp_l_z [in mod_opp_l_z]
ZEuclidProp.mod_mul_r [in mod_mul_r]
ZEuclidProp.mod_unique [in mod_unique]
ZEuclidProp.mod_opp_l_nz [in mod_opp_l_nz]
ZEuclidProp.mod_le [in mod_le]
ZEuclidProp.mod_add [in mod_add]
ZEuclidProp.mod_small [in mod_small]
ZEuclidProp.mod_mod [in mod_mod]
ZEuclidProp.mod_divides [in mod_divides]
ZEuclidProp.mod_eq [in mod_eq]
ZEuclidProp.mod_opp_r [in mod_opp_r]
ZEuclidProp.mod_0_l [in mod_0_l]
ZEuclidProp.mod_mul [in mod_mul]
ZEuclidProp.mod_opp_opp_nz [in mod_opp_opp_nz]
ZEuclidProp.mod_same [in mod_same]
ZEuclidProp.mod_opp_opp_z [in mod_opp_opp_z]
ZEuclidProp.mod_1_l [in mod_1_l]
ZEuclidProp.mul_succ_div_gt [in mul_succ_div_gt]
ZEuclidProp.mul_mod [in mul_mod]
ZEuclidProp.mul_mod_distr_r [in mul_mod_distr_r]
ZEuclidProp.mul_mod_distr_l [in mul_mod_distr_l]
ZEuclidProp.mul_mod_idemp_r [in mul_mod_idemp_r]
ZEuclidProp.mul_mod_idemp_l [in mul_mod_idemp_l]
ZEuclidProp.mul_pred_div_gt [in mul_pred_div_gt]
ZEuclidProp.mul_div_le [in mul_div_le]
ZEuclid.div_mod [in div_mod]
ZEuclid.mod_bound_pos [in mod_bound_pos]
ZEuclid.mod_always_pos [in mod_always_pos]
Zeven_odd_bool [in Zeven_odd_bool]
Zeven_bit_value [in Zeven_bit_value]
Zeven_mult_Zeven_l [in Zeven_mult_Zeven_l]
Zeven_pred [in Zeven_pred]
Zeven_div2 [in Zeven_div2]
Zeven_bool_iff [in Zeven_bool_iff]
Zeven_mult_Zeven_r [in Zeven_mult_Zeven_r]
Zeven_ex [in Zeven_ex]
Zeven_quot2 [in Zeven_quot2]
Zeven_plus_Zodd [in Zeven_plus_Zodd]
Zeven_equiv [in Zeven_equiv]
Zeven_not_Zodd [in Zeven_not_Zodd]
Zeven_mod [in Zeven_mod]
Zeven_plus_Zeven [in Zeven_plus_Zeven]
Zeven_2p [in Zeven_2p]
Zeven_Sn [in Zeven_Sn]
Zeven_ex_iff [in Zeven_ex_iff]
Zeven_rem [in Zeven_rem]
Zgcdn_opp [in Zgcdn_opp]
Zgcdn_is_gcd_pos [in Zgcdn_is_gcd_pos]
Zgcdn_ok_before_fibonacci [in Zgcdn_ok_before_fibonacci]
Zgcdn_pos [in Zgcdn_pos]
Zgcdn_is_gcd [in Zgcdn_is_gcd]
Zgcdn_linear_bound [in Zgcdn_linear_bound]
Zgcdn_worst_is_fibonacci [in Zgcdn_worst_is_fibonacci]
ZGcdProp.bezout_1_gcd [in bezout_1_gcd]
ZGcdProp.divide_1_r [in divide_1_r]
ZGcdProp.divide_opp_l [in divide_opp_l]
ZGcdProp.divide_antisym [in divide_antisym]
ZGcdProp.divide_opp_r [in divide_opp_r]
ZGcdProp.divide_abs_l [in divide_abs_l]
ZGcdProp.divide_mul_split [in divide_mul_split]
ZGcdProp.divide_add_cancel_r [in divide_add_cancel_r]
ZGcdProp.divide_1_r_abs [in divide_1_r_abs]
ZGcdProp.divide_sub_r [in divide_sub_r]
ZGcdProp.divide_antisym_abs [in divide_antisym_abs]
ZGcdProp.divide_abs_r [in divide_abs_r]
ZGcdProp.gauss [in gauss]
ZGcdProp.gcd_abs_l [in gcd_abs_l]
ZGcdProp.gcd_mul_mono_l [in gcd_mul_mono_l]
ZGcdProp.gcd_mul_mono_r_nonneg [in gcd_mul_mono_r_nonneg]
ZGcdProp.gcd_opp_r [in gcd_opp_r]
ZGcdProp.gcd_add_mult_diag_r [in gcd_add_mult_diag_r]
ZGcdProp.gcd_0_r [in gcd_0_r]
ZGcdProp.gcd_mul_mono_r [in gcd_mul_mono_r]
ZGcdProp.gcd_0_l [in gcd_0_l]
ZGcdProp.gcd_abs_r [in gcd_abs_r]
ZGcdProp.gcd_diag [in gcd_diag]
ZGcdProp.gcd_sub_diag_r [in gcd_sub_diag_r]
ZGcdProp.gcd_add_diag_r [in gcd_add_diag_r]
ZGcdProp.gcd_mul_mono_l_nonneg [in gcd_mul_mono_l_nonneg]
ZGcdProp.gcd_bezout [in gcd_bezout]
ZGcdProp.gcd_opp_l [in gcd_opp_l]
Zgcd_spec [in Zgcd_spec]
Zgcd_div_swap [in Zgcd_div_swap]
Zgcd_mult_rel_prime [in Zgcd_mult_rel_prime]
Zgcd_1_rel_prime [in Zgcd_1_rel_prime]
Zgcd_is_gcd [in Zgcd_is_gcd]
Zgcd_is_gcd [in Zgcd_is_gcd]
Zgcd_bound_fibonacci [in Zgcd_bound_fibonacci]
Zgcd_bound_opp [in Zgcd_bound_opp]
Zgcd_div_swap0 [in Zgcd_div_swap0]
Zgcd_bound [in Zgcd_bound]
Zgcd_alt_pos [in Zgcd_alt_pos]
Zgcd_div_pos [in Zgcd_div_pos]
Zgcd_ass [in Zgcd_ass]
Zge_cases [in Zge_cases]
Zge_is_le_bool [in Zge_is_le_bool]
Zge_left [in Zge_left]
Zge_compare [in Zge_compare]
Zge_trans [in Zge_trans]
Zge_minus_two_power_nat_S [in Zge_minus_two_power_nat_S]
Zgt_succ_pred [in Zgt_succ_pred]
Zgt_not_le [in Zgt_not_le]
Zgt_left [in Zgt_left]
Zgt_succ_le [in Zgt_succ_le]
Zgt_square_simpl [in Zgt_square_simpl]
Zgt_is_gt_bool [in Zgt_is_gt_bool]
Zgt_0_le_0_pred [in Zgt_0_le_0_pred]
Zgt_succ [in Zgt_succ]
Zgt_trans [in Zgt_trans]
Zgt_left_rev [in Zgt_left_rev]
Zgt_cases [in Zgt_cases]
Zgt_irrefl [in Zgt_irrefl]
Zgt_le_trans [in Zgt_le_trans]
Zgt_is_le_bool [in Zgt_is_le_bool]
Zgt_compare [in Zgt_compare]
Zgt_le_succ [in Zgt_le_succ]
Zgt_asym [in Zgt_asym]
Zgt_pos_0 [in Zgt_pos_0]
Zgt_succ_gt_or_eq [in Zgt_succ_gt_or_eq]
Zgt_left_gt [in Zgt_left_gt]
Zis_gcd_0 [in Zis_gcd_0]
Zis_gcd_1 [in Zis_gcd_1]
Zis_gcd_uniqueness_apart_sign [in Zis_gcd_uniqueness_apart_sign]
Zis_gcd_mod [in Zis_gcd_mod]
Zis_gcd_unique [in Zis_gcd_unique]
Zis_gcd_mult [in Zis_gcd_mult]
Zis_gcd_minus [in Zis_gcd_minus]
Zis_gcd_sym [in Zis_gcd_sym]
Zis_gcd_gcd [in Zis_gcd_gcd]
Zis_gcd_for_euclid [in Zis_gcd_for_euclid]
Zis_gcd_refl [in Zis_gcd_refl]
Zis_gcd_rel_prime [in Zis_gcd_rel_prime]
Zis_gcd_opp [in Zis_gcd_opp]
Zis_gcd_for_euclid2 [in Zis_gcd_for_euclid2]
Zis_gcd_0_abs [in Zis_gcd_0_abs]
Zis_gcd_bezout [in Zis_gcd_bezout]
ZLcmProp.divide_lcm_l [in divide_lcm_l]
ZLcmProp.divide_lcm_iff [in divide_lcm_iff]
ZLcmProp.divide_lcm_r [in divide_lcm_r]
ZLcmProp.divide_quot_mul_exact [in divide_quot_mul_exact]
ZLcmProp.divide_div [in divide_div]
ZLcmProp.divide_lcm_eq_r [in divide_lcm_eq_r]
ZLcmProp.divide_div_mul_exact [in divide_div_mul_exact]
ZLcmProp.gcd_1_lcm_mul [in gcd_1_lcm_mul]
ZLcmProp.gcd_quot_factor [in gcd_quot_factor]
ZLcmProp.gcd_quot_gcd [in gcd_quot_gcd]
ZLcmProp.gcd_div_factor [in gcd_div_factor]
ZLcmProp.gcd_rem [in gcd_rem]
ZLcmProp.gcd_div_gcd [in gcd_div_gcd]
ZLcmProp.gcd_div_swap [in gcd_div_swap]
ZLcmProp.gcd_mod [in gcd_mod]
ZLcmProp.lcm_abs_r [in lcm_abs_r]
ZLcmProp.lcm_1_l [in lcm_1_l]
ZLcmProp.lcm_diag_nonneg [in lcm_diag_nonneg]
ZLcmProp.lcm_0_l [in lcm_0_l]
ZLcmProp.lcm_0_r [in lcm_0_r]
ZLcmProp.lcm_least [in lcm_least]
ZLcmProp.lcm_1_l_nonneg [in lcm_1_l_nonneg]
ZLcmProp.lcm_equiv1 [in lcm_equiv1]
ZLcmProp.lcm_1_r [in lcm_1_r]
ZLcmProp.lcm_mul_mono_l [in lcm_mul_mono_l]
ZLcmProp.lcm_nonneg [in lcm_nonneg]
ZLcmProp.lcm_1_r_nonneg [in lcm_1_r_nonneg]
ZLcmProp.lcm_unique_alt [in lcm_unique_alt]
ZLcmProp.lcm_abs_l [in lcm_abs_l]
ZLcmProp.lcm_opp_r [in lcm_opp_r]
ZLcmProp.lcm_eq_0 [in lcm_eq_0]
ZLcmProp.lcm_unique [in lcm_unique]
ZLcmProp.lcm_divide_iff [in lcm_divide_iff]
ZLcmProp.lcm_assoc [in lcm_assoc]
ZLcmProp.lcm_equiv2 [in lcm_equiv2]
ZLcmProp.lcm_mul_mono_r_nonneg [in lcm_mul_mono_r_nonneg]
ZLcmProp.lcm_mul_mono_l_nonneg [in lcm_mul_mono_l_nonneg]
ZLcmProp.lcm_comm [in lcm_comm]
ZLcmProp.lcm_mul_mono_r [in lcm_mul_mono_r]
ZLcmProp.lcm_opp_l [in lcm_opp_l]
ZLcmProp.lcm_diag [in lcm_diag]
ZLcmProp.mod_divide [in mod_divide]
ZLcmProp.quot_div_nonneg [in quot_div_nonneg]
ZLcmProp.quot_div_exact [in quot_div_exact]
ZLcmProp.quot_div [in quot_div]
ZLcmProp.rem_mod [in rem_mod]
ZLcmProp.rem_divide [in rem_divide]
ZLcmProp.rem_mod_eq_0 [in rem_mod_eq_0]
ZLcmProp.rem_mod_nonneg [in rem_mod_nonneg]
Zlength_correct [in Zlength_correct]
Zlength_nil_inv [in Zlength_nil_inv]
Zlength_cons [in Zlength_cons]
Zlength_nil [in Zlength_nil]
Zle_bool_imp_le [in Zle_bool_imp_le]
Zle_bool_trans [in Zle_bool_trans]
Zle_succ_gt [in Zle_succ_gt]
Zle_bool_plus_mono [in Zle_bool_plus_mono]
Zle_neg_pos [in Zle_neg_pos]
Zle_left [in Zle_left]
Zle_0_minus_le [in Zle_0_minus_le]
Zle_gt_trans [in Zle_gt_trans]
Zle_cases [in Zle_cases]
Zle_bool_antisym [in Zle_bool_antisym]
Zle_is_le_bool [in Zle_is_le_bool]
Zle_imp_le_bool [in Zle_imp_le_bool]
Zle_0_nat [in Zle_0_nat]
Zle_minus_le_0 [in Zle_minus_le_0]
Zle_0_pos [in Zle_0_pos]
Zle_not_gt [in Zle_not_gt]
Zle_gt_succ [in Zle_gt_succ]
Zle_lt_succ [in Zle_lt_succ]
Zle_succ_le [in Zle_succ_le]
Zle_compare [in Zle_compare]
Zle_left_rev [in Zle_left_rev]
Zle_not_lt [in Zle_not_lt]
Zle_mult_approx [in Zle_mult_approx]
Zle_lt_or_eq [in Zle_lt_or_eq]
Zle_Qle [in Zle_Qle]
Zlog2_log_inf [in Zlog2_log_inf]
Zlog2_up_log_sup [in Zlog2_up_log_sup]
Zlt_compare [in Zlt_compare]
Zlt_succ_pred [in Zlt_succ_pred]
Zlt_left_rev [in Zlt_left_rev]
Zlt_0_le_0_pred [in Zlt_0_le_0_pred]
Zlt_not_le [in Zlt_not_le]
Zlt_two_power_nat_S [in Zlt_two_power_nat_S]
Zlt_cotrans_pos [in Zlt_cotrans_pos]
Zlt_left_lt [in Zlt_left_lt]
Zlt_lower_bound_rec [in Zlt_lower_bound_rec]
Zlt_cases [in Zlt_cases]
Zlt_le_succ [in Zlt_le_succ]
Zlt_lower_bound_ind [in Zlt_lower_bound_ind]
Zlt_left [in Zlt_left]
Zlt_is_le_bool [in Zlt_is_le_bool]
Zlt_cotrans_neg [in Zlt_cotrans_neg]
Zlt_square_simpl [in Zlt_square_simpl]
Zlt_0_minus_lt [in Zlt_0_minus_lt]
Zlt_is_lt_bool [in Zlt_is_lt_bool]
Zlt_succ_le [in Zlt_succ_le]
Zlt_Qlt [in Zlt_Qlt]
Zlt_cotrans [in Zlt_cotrans]
Zlt_neg_0 [in Zlt_neg_0]
Zlt_0_rec [in Zlt_0_rec]
Zlt_0_ind [in Zlt_0_ind]
Zlt0_not_eq [in Zlt0_not_eq]
ZL0 [in ZL0]
ZL6 [in ZL6]
ZMaxMinProp.add_max_distr_r [in add_max_distr_r]
ZMaxMinProp.add_min_distr_r [in add_min_distr_r]
ZMaxMinProp.add_min_distr_l [in add_min_distr_l]
ZMaxMinProp.add_max_distr_l [in add_max_distr_l]
ZMaxMinProp.mul_max_distr_nonpos_l [in mul_max_distr_nonpos_l]
ZMaxMinProp.mul_min_distr_nonneg_r [in mul_min_distr_nonneg_r]
ZMaxMinProp.mul_min_distr_nonpos_r [in mul_min_distr_nonpos_r]
ZMaxMinProp.mul_min_distr_nonneg_l [in mul_min_distr_nonneg_l]
ZMaxMinProp.mul_max_distr_nonneg_r [in mul_max_distr_nonneg_r]
ZMaxMinProp.mul_min_distr_nonpos_l [in mul_min_distr_nonpos_l]
ZMaxMinProp.mul_max_distr_nonpos_r [in mul_max_distr_nonpos_r]
ZMaxMinProp.mul_max_distr_nonneg_l [in mul_max_distr_nonneg_l]
ZMaxMinProp.opp_min_distr [in opp_min_distr]
ZMaxMinProp.opp_max_distr [in opp_max_distr]
ZMaxMinProp.pred_max_distr [in pred_max_distr]
ZMaxMinProp.pred_min_distr [in pred_min_distr]
ZMaxMinProp.sub_max_distr_r [in sub_max_distr_r]
ZMaxMinProp.sub_max_distr_l [in sub_max_distr_l]
ZMaxMinProp.sub_min_distr_l [in sub_min_distr_l]
ZMaxMinProp.sub_min_distr_r [in sub_min_distr_r]
ZMaxMinProp.succ_min_distr [in succ_min_distr]
ZMaxMinProp.succ_max_distr [in succ_max_distr]
Zmax_spec [in Zmax_spec]
Zmax_left [in Zmax_left]
Zminus_diag_reverse [in Zminus_diag_reverse]
Zminus_mod_idemp_r [in Zminus_mod_idemp_r]
Zminus_succ_l [in Zminus_succ_l]
Zminus_0_l_reverse [in Zminus_0_l_reverse]
Zminus_mod [in Zminus_mod]
Zminus_plus_simpl_l [in Zminus_plus_simpl_l]
Zminus_mod_idemp_l [in Zminus_mod_idemp_l]
Zminus_plus_simpl_r [in Zminus_plus_simpl_r]
Zminus_eq [in Zminus_eq]
Zminus_plus_simpl_l_reverse [in Zminus_plus_simpl_l_reverse]
Zmin_le_prime_inf [in Zmin_le_prime_inf]
Zmin_irreducible [in Zmin_irreducible]
Zmin_spec [in Zmin_spec]
Zmod_div_mod [in Zmod_div_mod]
Zmod_unique [in Zmod_unique]
Zmod_divide_minus [in Zmod_divide_minus]
Zmod_le_first [in Zmod_le_first]
Zmod_divide [in Zmod_divide]
Zmod_POS_correct [in Zmod_POS_correct]
Zmod_eq [in Zmod_eq]
Zmod_eq_full [in Zmod_eq_full]
Zmod_1_l [in Zmod_1_l]
Zmod_opp_opp [in Zmod_opp_opp]
Zmod_distr [in Zmod_distr]
Zmod_1_r [in Zmod_1_r]
Zmod_mod [in Zmod_mod]
Zmod_even [in Zmod_even]
Zmod_eqm [in Zmod_eqm]
Zmod_0_l [in Zmod_0_l]
Zmod_equal [in Zmod_equal]
Zmod_0_r [in Zmod_0_r]
Zmod_le [in Zmod_le]
Zmod_odd [in Zmod_odd]
Zmod_divides [in Zmod_divides]
Zmod_small [in Zmod_small]
Zmod_shift_r [in Zmod_shift_r]
Zmod_unique_full [in Zmod_unique_full]
Zmod'_correct [in Zmod'_correct]
Zmod2_twice [in Zmod2_twice]
ZMulOrderProp.eq_mul_1 [in eq_mul_1]
ZMulOrderProp.le_mul_diag_r [in le_mul_diag_r]
ZMulOrderProp.le_0_mul [in le_0_mul]
ZMulOrderProp.le_mul_0 [in le_mul_0]
ZMulOrderProp.le_mul_diag_l [in le_mul_diag_l]
ZMulOrderProp.lt_mul_diag_r [in lt_mul_diag_r]
ZMulOrderProp.lt_mul_0 [in lt_mul_0]
ZMulOrderProp.lt_mul_m1_neg [in lt_mul_m1_neg]
ZMulOrderProp.lt_1_mul_l [in lt_1_mul_l]
ZMulOrderProp.lt_mul_diag_l [in lt_mul_diag_l]
ZMulOrderProp.lt_mul_r [in lt_mul_r]
ZMulOrderProp.lt_m1_mul_r [in lt_m1_mul_r]
ZMulOrderProp.lt_1_mul_neg [in lt_1_mul_neg]
ZMulOrderProp.lt_mul_m1_pos [in lt_mul_m1_pos]
ZMulOrderProp.mul_nonneg_nonpos [in mul_nonneg_nonpos]
ZMulOrderProp.mul_le_mono_nonpos [in mul_le_mono_nonpos]
ZMulOrderProp.mul_nonpos_nonpos [in mul_nonpos_nonpos]
ZMulOrderProp.mul_lt_mono_nonpos [in mul_lt_mono_nonpos]
ZMulOrderProp.mul_nonpos_nonneg [in mul_nonpos_nonneg]
ZMulOrderProp.nlt_square_0 [in nlt_square_0]
ZMulOrderProp.square_lt_simpl_nonpos [in square_lt_simpl_nonpos]
ZMulOrderProp.square_le_mono_nonpos [in square_le_mono_nonpos]
ZMulOrderProp.square_le_simpl_nonpos [in square_le_simpl_nonpos]
ZMulOrderProp.square_lt_mono_nonpos [in square_lt_mono_nonpos]
ZMulProp.mul_sub_distr_r [in mul_sub_distr_r]
ZMulProp.mul_pred_r [in mul_pred_r]
ZMulProp.mul_sub_distr_l [in mul_sub_distr_l]
ZMulProp.mul_opp_r [in mul_opp_r]
ZMulProp.mul_pred_l [in mul_pred_l]
ZMulProp.mul_opp_comm [in mul_opp_comm]
ZMulProp.mul_opp_l [in mul_opp_l]
ZMulProp.mul_opp_opp [in mul_opp_opp]
Zmult_ge_reg_r [in Zmult_ge_reg_r]
Zmult_gt_0_lt_compat_l [in Zmult_gt_0_lt_compat_l]
Zmult_lt_0_reg_r_2 [in Zmult_lt_0_reg_r_2]
Zmult_one [in Zmult_one]
Zmult_integral [in Zmult_integral]
Zmult_mod_distr_r [in Zmult_mod_distr_r]
Zmult_le_0_reg_r [in Zmult_le_0_reg_r]
Zmult_succ_r_reverse [in Zmult_succ_r_reverse]
Zmult_mod_idemp_r [in Zmult_mod_idemp_r]
Zmult_gt_reg_r [in Zmult_gt_reg_r]
Zmult_gt_compat_r [in Zmult_gt_compat_r]
Zmult_gt_0_le_compat_r [in Zmult_gt_0_le_compat_r]
Zmult_rem_distr_l [in Zmult_rem_distr_l]
Zmult_lt_compat [in Zmult_lt_compat]
Zmult_ge_compat_l [in Zmult_ge_compat_l]
Zmult_assoc_reverse [in Zmult_assoc_reverse]
Zmult_gt_compat_l [in Zmult_gt_compat_l]
Zmult_lt_0_reg_r [in Zmult_lt_0_reg_r]
Zmult_lt_reg_r [in Zmult_lt_reg_r]
Zmult_lt_0_le_compat_r [in Zmult_lt_0_le_compat_r]
Zmult_le_reg_r [in Zmult_le_reg_r]
Zmult_lt_b [in Zmult_lt_b]
Zmult_le_compat_r [in Zmult_le_compat_r]
Zmult_ge_compat_r [in Zmult_ge_compat_r]
Zmult_gt_0_lt_reg_r [in Zmult_gt_0_lt_reg_r]
Zmult_lt_compat_l [in Zmult_lt_compat_l]
Zmult_rem_idemp_l [in Zmult_rem_idemp_l]
Zmult_mod_distr_l [in Zmult_mod_distr_l]
Zmult_gt_0_le_0_compat [in Zmult_gt_0_le_0_compat]
Zmult_gt_0_compat [in Zmult_gt_0_compat]
Zmult_rem_distr_r [in Zmult_rem_distr_r]
Zmult_le_approx [in Zmult_le_approx]
Zmult_rem [in Zmult_rem]
Zmult_0_r_reverse [in Zmult_0_r_reverse]
Zmult_gt_0_lt_compat_r [in Zmult_gt_0_lt_compat_r]
Zmult_power [in Zmult_power]
Zmult_mod [in Zmult_mod]
Zmult_lt_compat2 [in Zmult_lt_compat2]
Zmult_succ_l_reverse [in Zmult_succ_l_reverse]
Zmult_compare_compat_l [in Zmult_compare_compat_l]
Zmult_minus_distr_l [in Zmult_minus_distr_l]
Zmult_integral_l [in Zmult_integral_l]
Zmult_ge_compat [in Zmult_ge_compat]
Zmult_le_compat [in Zmult_le_compat]
Zmult_lt_0_le_reg_r [in Zmult_lt_0_le_reg_r]
Zmult_lt_compat_r [in Zmult_lt_compat_r]
Zmult_compare_compat_r [in Zmult_compare_compat_r]
Zmult_mod_idemp_l [in Zmult_mod_idemp_l]
Zmult_gt_0_lt_0_reg_r [in Zmult_gt_0_lt_0_reg_r]
Zmult_le_compat_l [in Zmult_le_compat_l]
Zmult_rem_idemp_r [in Zmult_rem_idemp_r]
Zmult_gt_0_reg_l [in Zmult_gt_0_reg_l]
Zne_left [in Zne_left]
Znot_le_succ [in Znot_le_succ]
Znot_ge_lt [in Znot_ge_lt]
Znot_lt_ge [in Znot_lt_ge]
Znot_le_gt [in Znot_le_gt]
Znot_gt_le [in Znot_gt_le]
ZnZ.of_Z_correct [in of_Z_correct]
ZnZ.of_pos_correct [in of_pos_correct]
ZnZ.spec_OW [in spec_OW]
ZnZ.spec_WW [in spec_WW]
ZnZ.spec_WO [in spec_WO]
Zodd_bool_iff [in Zodd_bool_iff]
Zodd_quot2 [in Zodd_quot2]
Zodd_quot2_neg [in Zodd_quot2_neg]
Zodd_plus_Zodd [in Zodd_plus_Zodd]
Zodd_pred [in Zodd_pred]
Zodd_ex_iff [in Zodd_ex_iff]
Zodd_Sn [in Zodd_Sn]
Zodd_mult_Zodd [in Zodd_mult_Zodd]
Zodd_rem [in Zodd_rem]
Zodd_equiv [in Zodd_equiv]
Zodd_plus_Zeven [in Zodd_plus_Zeven]
Zodd_bit_value [in Zodd_bit_value]
Zodd_div2 [in Zodd_div2]
Zodd_2p_plus_1 [in Zodd_2p_plus_1]
Zodd_mod [in Zodd_mod]
Zodd_ex [in Zodd_ex]
Zodd_not_Zeven [in Zodd_not_Zeven]
Zodd_even_bool [in Zodd_even_bool]
Zone_min_pos [in Zone_min_pos]
Zone_pos [in Zone_pos]
Zopp_mult_distr_l [in Zopp_mult_distr_l]
Zopp_mult_distr_r [in Zopp_mult_distr_r]
ZOrderProp.le_le_pred [in le_le_pred]
ZOrderProp.le_pred_lt_succ [in le_pred_lt_succ]
ZOrderProp.le_succ_le_pred [in le_succ_le_pred]
ZOrderProp.le_pred_l [in le_pred_l]
ZOrderProp.le_pred_lt [in le_pred_lt]
ZOrderProp.lt_m1_r [in lt_m1_r]
ZOrderProp.lt_pred_le [in lt_pred_le]
ZOrderProp.lt_pred_l [in lt_pred_l]
ZOrderProp.lt_pred_lt [in lt_pred_lt]
ZOrderProp.lt_le_pred [in lt_le_pred]
ZOrderProp.lt_succ_lt_pred [in lt_succ_lt_pred]
ZOrderProp.lt_lt_pred [in lt_lt_pred]
ZOrderProp.lt_pred_lt_succ [in lt_pred_lt_succ]
ZOrderProp.neg_nonneg_cases [in neg_nonneg_cases]
ZOrderProp.neg_pos_cases [in neg_pos_cases]
ZOrderProp.neq_pred_l [in neq_pred_l]
ZOrderProp.nle_pred_r [in nle_pred_r]
ZOrderProp.nonpos_pos_cases [in nonpos_pos_cases]
ZOrderProp.nonpos_nonneg_cases [in nonpos_nonneg_cases]
ZOrderProp.pred_lt_mono [in pred_lt_mono]
ZOrderProp.pred_le_mono [in pred_le_mono]
ZPairsAxiomsMod.add_succ_l [in add_succ_l]
ZPairsAxiomsMod.add_0_l [in add_0_l]
ZPairsAxiomsMod.bi_induction [in bi_induction]
ZPairsAxiomsMod.lt_irrefl [in lt_irrefl]
ZPairsAxiomsMod.lt_eq_cases [in lt_eq_cases]
ZPairsAxiomsMod.lt_nge [in lt_nge]
ZPairsAxiomsMod.lt_succ_r [in lt_succ_r]
ZPairsAxiomsMod.max_r [in max_r]
ZPairsAxiomsMod.max_l [in max_l]
ZPairsAxiomsMod.min_r [in min_r]
ZPairsAxiomsMod.min_l [in min_l]
ZPairsAxiomsMod.mul_succ_l [in mul_succ_l]
ZPairsAxiomsMod.mul_0_l [in mul_0_l]
ZPairsAxiomsMod.mul_comm [in mul_comm]
ZPairsAxiomsMod.one_succ [in one_succ]
ZPairsAxiomsMod.opp_succ [in opp_succ]
ZPairsAxiomsMod.opp_0 [in opp_0]
ZPairsAxiomsMod.pred_succ [in pred_succ]
ZPairsAxiomsMod.sub_add_opp [in sub_add_opp]
ZPairsAxiomsMod.sub_succ_r [in sub_succ_r]
ZPairsAxiomsMod.sub_0_r [in sub_0_r]
ZPairsAxiomsMod.succ_pred [in succ_pred]
ZPairsAxiomsMod.two_succ [in two_succ]
ZParityProp.even_sub [in even_sub]
ZParityProp.even_opp [in even_opp]
ZParityProp.even_pred [in even_pred]
ZParityProp.odd_opp [in odd_opp]
ZParityProp.odd_sub [in odd_sub]
ZParityProp.odd_pred [in odd_pred]
Zplus_minus_eq [in Zplus_minus_eq]
Zplus_mod [in Zplus_mod]
Zplus_lt_compat_l [in Zplus_lt_compat_l]
Zplus_compare_compat [in Zplus_compare_compat]
Zplus_rem_idemp_r [in Zplus_rem_idemp_r]
Zplus_rem_idemp_l [in Zplus_rem_idemp_l]
Zplus_lt_compat_r [in Zplus_lt_compat_r]
Zplus_eq_compat [in Zplus_eq_compat]
Zplus_0_r_reverse [in Zplus_0_r_reverse]
Zplus_mod_one [in Zplus_mod_one]
Zplus_le_compat_r [in Zplus_le_compat_r]
Zplus_gt_compat_r [in Zplus_gt_compat_r]
Zplus_assoc_reverse [in Zplus_assoc_reverse]
Zplus_diag_eq_mult_2 [in Zplus_diag_eq_mult_2]
Zplus_mod_idemp_l [in Zplus_mod_idemp_l]
Zplus_lt_reg_l [in Zplus_lt_reg_l]
Zplus_rem [in Zplus_rem]
Zplus_gt_reg_l [in Zplus_gt_reg_l]
Zplus_gt_reg_r [in Zplus_gt_reg_r]
Zplus_lt_reg_r [in Zplus_lt_reg_r]
Zplus_le_reg_l [in Zplus_le_reg_l]
Zplus_gt_compat_l [in Zplus_gt_compat_l]
Zplus_succ_r_reverse [in Zplus_succ_r_reverse]
Zplus_le_reg_r [in Zplus_le_reg_r]
Zplus_mod_idemp_r [in Zplus_mod_idemp_r]
Zplus_le_compat_l [in Zplus_le_compat_l]
Zplus_minus [in Zplus_minus]
Zpos_P_of_succ_nat [in Zpos_P_of_succ_nat]
Zpos_min_1 [in Zpos_min_1]
Zpos_max_1 [in Zpos_max_1]
Zpos_eq [in Zpos_eq]
Zpos_eq_iff [in Zpos_eq_iff]
Zpower_NR0 [in Zpower_NR0]
Zpower_nat_0_r [in Zpower_nat_0_r]
Zpower_nat_is_exp [in Zpower_nat_is_exp]
Zpower_le_monotone3 [in Zpower_le_monotone3]
Zpower_nat_Zpower [in Zpower_nat_Zpower]
Zpower_nat_powerRZ [in Zpower_nat_powerRZ]
Zpower_nat_Z [in Zpower_nat_Z]
Zpower_alt_neg_r [in Zpower_alt_neg_r]
Zpower_alt_0_r [in Zpower_alt_0_r]
Zpower_exp [in Zpower_exp]
Zpower_theory [in Zpower_theory]
Zpower_mod [in Zpower_mod]
Zpower_gt_1 [in Zpower_gt_1]
Zpower_pos_1_r [in Zpower_pos_1_r]
Zpower_equiv [in Zpower_equiv]
Zpower_pos_nat [in Zpower_pos_nat]
Zpower_pos_is_exp [in Zpower_pos_is_exp]
Zpower_le_monotone_inv [in Zpower_le_monotone_inv]
Zpower_alt_Ppow [in Zpower_alt_Ppow]
Zpower_le_monotone [in Zpower_le_monotone]
Zpower_Qpower [in Zpower_Qpower]
Zpower_pos_powerRZ [in Zpower_pos_powerRZ]
Zpower_pos_0_l [in Zpower_pos_0_l]
Zpower_alt_succ_r [in Zpower_alt_succ_r]
Zpower_nat_succ_r [in Zpower_nat_succ_r]
Zpower_divide [in Zpower_divide]
Zpower_pos_1_l [in Zpower_pos_1_l]
Zpower_nat_powerRZ_absolu [in Zpower_nat_powerRZ_absolu]
Zpower_pos_pos [in Zpower_pos_pos]
Zpower_lt_monotone [in Zpower_lt_monotone]
Zpower2_le_lin [in Zpower2_le_lin]
Zpower2_Psize [in Zpower2_Psize]
Zpower2_lt_lin [in Zpower2_lt_lin]
ZPowProp.abs_pow [in abs_pow]
ZPowProp.even_pow [in even_pow]
ZPowProp.odd_pow [in odd_pow]
ZPowProp.pow_opp_odd [in pow_opp_odd]
ZPowProp.pow_twice_r [in pow_twice_r]
ZPowProp.pow_odd_abs_sgn [in pow_odd_abs_sgn]
ZPowProp.pow_odd_sgn [in pow_odd_sgn]
ZPowProp.pow_even_nonneg [in pow_even_nonneg]
ZPowProp.pow_opp_even [in pow_opp_even]
ZPowProp.pow_even_abs [in pow_even_abs]
Zpow_mod_pos_correct [in Zpow_mod_pos_correct]
Zpow_mod_correct [in Zpow_mod_correct]
Zpred_succ [in Zpred_succ]
ZQuotProp.add_rem_idemp_l [in add_rem_idemp_l]
ZQuotProp.add_rem [in add_rem]
ZQuotProp.add_rem_idemp_r [in add_rem_idemp_r]
ZQuotProp.mod_mul_r [in mod_mul_r]
ZQuotProp.mul_rem [in mul_rem]
ZQuotProp.mul_rem_distr_r [in mul_rem_distr_r]
ZQuotProp.mul_rem_idemp_l [in mul_rem_idemp_l]
ZQuotProp.mul_pred_quot_lt [in mul_pred_quot_lt]
ZQuotProp.mul_succ_quot_gt [in mul_succ_quot_gt]
ZQuotProp.mul_rem_idemp_r [in mul_rem_idemp_r]
ZQuotProp.mul_rem_distr_l [in mul_rem_distr_l]
ZQuotProp.mul_quot_le [in mul_quot_le]
ZQuotProp.mul_pred_quot_gt [in mul_pred_quot_gt]
ZQuotProp.mul_quot_ge [in mul_quot_ge]
ZQuotProp.mul_succ_quot_lt [in mul_succ_quot_lt]
ZQuotProp.quot_opp_l [in quot_opp_l]
ZQuotProp.quot_unique_exact [in quot_unique_exact]
ZQuotProp.quot_le_upper_bound [in quot_le_upper_bound]
ZQuotProp.quot_unique [in quot_unique]
ZQuotProp.quot_lt_upper_bound [in quot_lt_upper_bound]
ZQuotProp.quot_small_iff [in quot_small_iff]
ZQuotProp.quot_opp_r [in quot_opp_r]
ZQuotProp.quot_mul [in quot_mul]
ZQuotProp.quot_add [in quot_add]
ZQuotProp.quot_opp_opp [in quot_opp_opp]
ZQuotProp.quot_small [in quot_small]
ZQuotProp.quot_le_compat_l [in quot_le_compat_l]
ZQuotProp.quot_mul_cancel_r [in quot_mul_cancel_r]
ZQuotProp.quot_0_l [in quot_0_l]
ZQuotProp.quot_same [in quot_same]
ZQuotProp.quot_abs_l [in quot_abs_l]
ZQuotProp.quot_add_l [in quot_add_l]
ZQuotProp.quot_le_mono [in quot_le_mono]
ZQuotProp.quot_lt [in quot_lt]
ZQuotProp.quot_abs [in quot_abs]
ZQuotProp.quot_mul_cancel_l [in quot_mul_cancel_l]
ZQuotProp.quot_abs_r [in quot_abs_r]
ZQuotProp.quot_exact [in quot_exact]
ZQuotProp.quot_mul_le [in quot_mul_le]
ZQuotProp.quot_pos [in quot_pos]
ZQuotProp.quot_str_pos [in quot_str_pos]
ZQuotProp.quot_le_lower_bound [in quot_le_lower_bound]
ZQuotProp.quot_rem_unique [in quot_rem_unique]
ZQuotProp.quot_1_r [in quot_1_r]
ZQuotProp.quot_quot [in quot_quot]
ZQuotProp.quot_1_l [in quot_1_l]
ZQuotProp.rem_sign_nz [in rem_sign_nz]
ZQuotProp.rem_sign [in rem_sign]
ZQuotProp.rem_same [in rem_same]
ZQuotProp.rem_1_l [in rem_1_l]
ZQuotProp.rem_abs [in rem_abs]
ZQuotProp.rem_small_iff [in rem_small_iff]
ZQuotProp.rem_eq [in rem_eq]
ZQuotProp.rem_bound_abs [in rem_bound_abs]
ZQuotProp.rem_mul [in rem_mul]
ZQuotProp.rem_opp_opp [in rem_opp_opp]
ZQuotProp.rem_0_l [in rem_0_l]
ZQuotProp.rem_rem [in rem_rem]
ZQuotProp.rem_le [in rem_le]
ZQuotProp.rem_abs_l [in rem_abs_l]
ZQuotProp.rem_abs_r [in rem_abs_r]
ZQuotProp.rem_unique [in rem_unique]
ZQuotProp.rem_add [in rem_add]
ZQuotProp.rem_1_r [in rem_1_r]
ZQuotProp.rem_small [in rem_small]
ZQuotProp.rem_nonpos [in rem_nonpos]
ZQuotProp.rem_sign_mul [in rem_sign_mul]
ZQuotProp.rem_nonneg [in rem_nonneg]
Zquotrem_Zdiv_eucl_pos [in Zquotrem_Zdiv_eucl_pos]
Zquot_Zdiv_pos [in Zquot_Zdiv_pos]
Zquot_mult_le [in Zquot_mult_le]
Zquot_sgn [in Zquot_sgn]
Zquot_0_r [in Zquot_0_r]
Zquot_mod_unique_full [in Zquot_mod_unique_full]
Zquot_mult_cancel_l [in Zquot_mult_cancel_l]
Zquot_lt_upper_bound [in Zquot_lt_upper_bound]
Zquot_le_lower_bound [in Zquot_le_lower_bound]
Zquot_Zquot [in Zquot_Zquot]
Zquot_le_upper_bound [in Zquot_le_upper_bound]
Zquot_mult_cancel_r [in Zquot_mult_cancel_r]
Zquot_0_l [in Zquot_0_l]
Zquot_unique_full [in Zquot_unique_full]
Zquot_opp_opp [in Zquot_opp_opp]
Zquot_opp_r [in Zquot_opp_r]
Zquot_opp_l [in Zquot_opp_l]
Zquot2_opp [in Zquot2_opp]
Zquot2_odd_remainder [in Zquot2_odd_remainder]
Zquot2_quot [in Zquot2_quot]
Zquot2_odd_eqn [in Zquot2_odd_eqn]
Zrel_prime_neq_mod_0 [in Zrel_prime_neq_mod_0]
Zrem_Zmod_pos [in Zrem_Zmod_pos]
Zrem_lt_neg_neg [in Zrem_lt_neg_neg]
Zrem_sgn [in Zrem_sgn]
Zrem_sgn2 [in Zrem_sgn2]
Zrem_le [in Zrem_le]
Zrem_unique_full [in Zrem_unique_full]
Zrem_lt_pos_pos [in Zrem_lt_pos_pos]
Zrem_lt_neg [in Zrem_lt_neg]
Zrem_Zmod_zero [in Zrem_Zmod_zero]
Zrem_0_l [in Zrem_0_l]
Zrem_opp_opp [in Zrem_opp_opp]
Zrem_lt_neg_pos [in Zrem_lt_neg_pos]
Zrem_even [in Zrem_even]
Zrem_lt_pos_neg [in Zrem_lt_pos_neg]
Zrem_odd [in Zrem_odd]
Zrem_lt_pos [in Zrem_lt_pos]
Zrem_0_r [in Zrem_0_r]
Zrem_rem [in Zrem_rem]
Zrem_opp_r [in Zrem_opp_r]
Zrem_opp_l [in Zrem_opp_l]
Zrem_divides [in Zrem_divides]
ZSgnAbsProp.abs_involutive [in abs_involutive]
ZSgnAbsProp.abs_eq_iff [in abs_eq_iff]
ZSgnAbsProp.abs_max [in abs_max]
ZSgnAbsProp.abs_neq_iff [in abs_neq_iff]
ZSgnAbsProp.abs_square [in abs_square]
ZSgnAbsProp.abs_case_strong [in abs_case_strong]
ZSgnAbsProp.abs_sgn [in abs_sgn]
ZSgnAbsProp.abs_nonneg [in abs_nonneg]
ZSgnAbsProp.abs_eq_or_opp [in abs_eq_or_opp]
ZSgnAbsProp.abs_lt [in abs_lt]
ZSgnAbsProp.abs_neq' [in abs_neq']
ZSgnAbsProp.abs_0_iff [in abs_0_iff]
ZSgnAbsProp.abs_spec [in abs_spec]
ZSgnAbsProp.abs_triangle [in abs_triangle]
ZSgnAbsProp.abs_eq_cases [in abs_eq_cases]
ZSgnAbsProp.abs_le [in abs_le]
ZSgnAbsProp.abs_case [in abs_case]
ZSgnAbsProp.abs_pos [in abs_pos]
ZSgnAbsProp.abs_mul [in abs_mul]
ZSgnAbsProp.abs_opp [in abs_opp]
ZSgnAbsProp.abs_sub_triangle [in abs_sub_triangle]
ZSgnAbsProp.abs_0 [in abs_0]
ZSgnAbsProp.abs_or_opp_abs [in abs_or_opp_abs]
ZSgnAbsProp.sgn_null_iff [in sgn_null_iff]
ZSgnAbsProp.sgn_nonpos [in sgn_nonpos]
ZSgnAbsProp.sgn_nonneg [in sgn_nonneg]
ZSgnAbsProp.sgn_opp [in sgn_opp]
ZSgnAbsProp.sgn_abs [in sgn_abs]
ZSgnAbsProp.sgn_sgn [in sgn_sgn]
ZSgnAbsProp.sgn_pos_iff [in sgn_pos_iff]
ZSgnAbsProp.sgn_mul [in sgn_mul]
ZSgnAbsProp.sgn_neg_iff [in sgn_neg_iff]
ZSgnAbsProp.sgn_spec [in sgn_spec]
ZSgnAbsProp.sgn_0 [in sgn_0]
Zsgn_spec [in Zsgn_spec]
Zsplit2 [in Zsplit2]
Zsqrt_interval [in Zsqrt_interval]
Zsqrt_square_id [in Zsqrt_square_id]
Zsqrt_equiv [in Zsqrt_equiv]
Zsqrt_le [in Zsqrt_le]
Zsqrt_plain_is_pos [in Zsqrt_plain_is_pos]
Zsquare_mult [in Zsquare_mult]
Zsquare_le [in Zsquare_le]
Zsquare_pos [in Zsquare_pos]
Zsucc_lt_compat [in Zsucc_lt_compat]
Zsucc_le_reg [in Zsucc_le_reg]
Zsucc_lt_reg [in Zsucc_lt_reg]
Zsucc_gt_reg [in Zsucc_gt_reg]
Zsucc_eq_compat [in Zsucc_eq_compat]
Zsucc_le_compat [in Zsucc_le_compat]
Zsucc_pred [in Zsucc_pred]
Zsucc_gt_compat [in Zsucc_gt_compat]
Ztrichotomy [in Ztrichotomy]
Ztrichotomy_inf [in Ztrichotomy_inf]
ZTypeIsZAxioms.abs_eq [in abs_eq]
ZTypeIsZAxioms.abs_neq [in abs_neq]
ZTypeIsZAxioms.add_succ_l [in add_succ_l]
ZTypeIsZAxioms.add_0_l [in add_0_l]
ZTypeIsZAxioms.bi_induction [in bi_induction]
ZTypeIsZAxioms.BP [in BP]
ZTypeIsZAxioms.BS [in BS]
ZTypeIsZAxioms.B_holds [in B_holds]
ZTypeIsZAxioms.B0 [in B0]
ZTypeIsZAxioms.compare_lt_iff [in compare_lt_iff]
ZTypeIsZAxioms.compare_antisym [in compare_antisym]
ZTypeIsZAxioms.compare_le_iff [in compare_le_iff]
ZTypeIsZAxioms.compare_eq_iff [in compare_eq_iff]
ZTypeIsZAxioms.div_mod [in div_mod]
ZTypeIsZAxioms.div2_spec [in div2_spec]
ZTypeIsZAxioms.eqb_eq [in eqb_eq]
ZTypeIsZAxioms.even_spec [in even_spec]
ZTypeIsZAxioms.gcd_nonneg [in gcd_nonneg]
ZTypeIsZAxioms.gcd_greatest [in gcd_greatest]
ZTypeIsZAxioms.gcd_divide_r [in gcd_divide_r]
ZTypeIsZAxioms.gcd_divide_l [in gcd_divide_l]
ZTypeIsZAxioms.land_spec [in land_spec]
ZTypeIsZAxioms.ldiff_spec [in ldiff_spec]
ZTypeIsZAxioms.leb_le [in leb_le]
ZTypeIsZAxioms.log2_spec [in log2_spec]
ZTypeIsZAxioms.log2_nonpos [in log2_nonpos]
ZTypeIsZAxioms.lor_spec [in lor_spec]
ZTypeIsZAxioms.ltb_lt [in ltb_lt]
ZTypeIsZAxioms.lt_succ_r [in lt_succ_r]
ZTypeIsZAxioms.lxor_spec [in lxor_spec]
ZTypeIsZAxioms.max_r [in max_r]
ZTypeIsZAxioms.max_l [in max_l]
ZTypeIsZAxioms.min_r [in min_r]
ZTypeIsZAxioms.min_l [in min_l]
ZTypeIsZAxioms.mod_neg_bound [in mod_neg_bound]
ZTypeIsZAxioms.mod_pos_bound [in mod_pos_bound]
ZTypeIsZAxioms.mul_succ_l [in mul_succ_l]
ZTypeIsZAxioms.mul_0_l [in mul_0_l]
ZTypeIsZAxioms.odd_spec [in odd_spec]
ZTypeIsZAxioms.one_succ [in one_succ]
ZTypeIsZAxioms.opp_succ [in opp_succ]
ZTypeIsZAxioms.opp_0 [in opp_0]
ZTypeIsZAxioms.pow_pow_N [in pow_pow_N]
ZTypeIsZAxioms.pow_0_r [in pow_0_r]
ZTypeIsZAxioms.pow_pos_N [in pow_pos_N]
ZTypeIsZAxioms.pow_succ_r [in pow_succ_r]
ZTypeIsZAxioms.pow_neg_r [in pow_neg_r]
ZTypeIsZAxioms.pred_succ [in pred_succ]
ZTypeIsZAxioms.quot_rem [in quot_rem]
ZTypeIsZAxioms.rem_opp_l [in rem_opp_l]
ZTypeIsZAxioms.rem_bound_pos [in rem_bound_pos]
ZTypeIsZAxioms.rem_opp_r [in rem_opp_r]
ZTypeIsZAxioms.sgn_pos [in sgn_pos]
ZTypeIsZAxioms.sgn_null [in sgn_null]
ZTypeIsZAxioms.sgn_neg [in sgn_neg]
ZTypeIsZAxioms.shiftl_spec_low [in shiftl_spec_low]
ZTypeIsZAxioms.shiftl_spec_high [in shiftl_spec_high]
ZTypeIsZAxioms.shiftr_spec [in shiftr_spec]
ZTypeIsZAxioms.spec_divide [in spec_divide]
ZTypeIsZAxioms.sqrt_spec [in sqrt_spec]
ZTypeIsZAxioms.sqrt_neg [in sqrt_neg]
ZTypeIsZAxioms.square_spec [in square_spec]
ZTypeIsZAxioms.sub_succ_r [in sub_succ_r]
ZTypeIsZAxioms.sub_0_r [in sub_0_r]
ZTypeIsZAxioms.succ_pred [in succ_pred]
ZTypeIsZAxioms.testbit_even_0 [in testbit_even_0]
ZTypeIsZAxioms.testbit_neg_r [in testbit_neg_r]
ZTypeIsZAxioms.testbit_even_succ [in testbit_even_succ]
ZTypeIsZAxioms.testbit_odd_0 [in testbit_odd_0]
ZTypeIsZAxioms.testbit_odd_succ [in testbit_odd_succ]
ZTypeIsZAxioms.two_succ [in two_succ]
Zwf_up_well_founded [in Zwf_up_well_founded]
Zwf_well_founded [in Zwf_well_founded]
Z_div_mod_eq [in Z_div_mod_eq]
Z_R_minus [in Z_R_minus]
Z_quot_lt [in Z_quot_lt]
Z_lt_abs_induction [in Z_lt_abs_induction]
Z_div_lt [in Z_div_lt]
Z_zerop [in Z_zerop]
Z_as_Int.i2z_2 [in i2z_2]
Z_notzerop [in Z_notzerop]
Z_of_nat_complete [in Z_of_nat_complete]
Z_mod_lt [in Z_mod_lt]
Z_div2_value [in Z_div2_value]
Z_div_plus_full [in Z_div_plus_full]
Z_mod_nz_opp_r [in Z_mod_nz_opp_r]
Z_mod_mult [in Z_mod_mult]
Z_rem_same [in Z_rem_same]
Z_dec [in Z_dec]
Z_div_zero_opp_r [in Z_div_zero_opp_r]
Z_as_Int.i2z_mult [in i2z_mult]
Z_div_nz_opp_r [in Z_div_nz_opp_r]
Z_div_plus [in Z_div_plus]
Z_as_Int.i2z_max [in i2z_max]
Z_div_same_full [in Z_div_same_full]
Z_div_exact_2 [in Z_div_exact_2]
Z_div_exact_full_2 [in Z_div_exact_full_2]
Z_0_1_more [in Z_0_1_more]
Z_div_mod_POS [in Z_div_mod_POS]
Z_as_Int.i2z_eq [in i2z_eq]
Z_to_binary [in Z_to_binary]
Z_mult_div_ge_neg [in Z_mult_div_ge_neg]
Z_nat_N [in Z_nat_N]
Z_div_pos [in Z_div_pos]
Z_mod_zero_opp_full [in Z_mod_zero_opp_full]
Z_mod_plus [in Z_mod_plus]
Z_N_nat [in Z_N_nat]
Z_mod_remainder [in Z_mod_remainder]
Z_div_mod [in Z_div_mod]
Z_div_plus_full_l [in Z_div_plus_full_l]
Z_to_binary_to_Z [in Z_to_binary_to_Z]
Z_to_two_compl_to_Z [in Z_to_two_compl_to_Z]
Z_mod_zero_opp [in Z_mod_zero_opp]
Z_mod_nz_opp_full [in Z_mod_nz_opp_full]
Z_lt_induction [in Z_lt_induction]
Z_as_Int.i2z_1 [in i2z_1]
Z_mod_neg [in Z_mod_neg]
Z_mult_div_ge [in Z_mult_div_ge]
Z_div_le [in Z_div_le]
Z_mod_same_full [in Z_mod_same_full]
Z_of_nat_prop [in Z_of_nat_prop]
Z_div_mult [in Z_div_mult]
Z_of_nat_set [in Z_of_nat_set]
Z_as_Int.i2z_plus [in i2z_plus]
Z_rem_mult [in Z_rem_mult]
Z_as_Int.i2z_0 [in i2z_0]
Z_div_same [in Z_div_same]
Z_of_nat_complete_inf [in Z_of_nat_complete_inf]
Z_div_exact_full_1 [in Z_div_exact_full_1]
Z_div_nz_opp_full [in Z_div_nz_opp_full]
Z_div_ge [in Z_div_ge]
Z_noteq_dec [in Z_noteq_dec]
Z_quot_plus_l [in Z_quot_plus_l]
Z_div_mult_full [in Z_div_mult_full]
Z_mod_plus_full [in Z_mod_plus_full]
Z_quot_pos [in Z_quot_pos]
Z_quot_plus [in Z_quot_plus]
Z_as_OT.lt_not_eq [in lt_not_eq]
Z_lt_abs_rec [in Z_lt_abs_rec]
Z_as_Int.i2z_minus [in i2z_minus]
Z_div_zero_opp_full [in Z_div_zero_opp_full]
Z_to_two_compl_Sn [in Z_to_two_compl_Sn]
Z_as_OT.lt_trans [in lt_trans]
Z_as_Int.i2z_3 [in i2z_3]
Z_lt_le_dec [in Z_lt_le_dec]
Z_rem_plus [in Z_rem_plus]
Z_quot_monotone [in Z_quot_monotone]
Z_to_binary_Sn_z [in Z_to_binary_Sn_z]
Z_div_exact_1 [in Z_div_exact_1]
Z_to_two_compl_Sn_z [in Z_to_two_compl_Sn_z]
Z_eq_mult [in Z_eq_mult]
Z_quot_exact_full [in Z_quot_exact_full]
Z_lt_rec [in Z_lt_rec]
Z_to_two_compl [in Z_to_two_compl]
Z_dec' [in Z_dec']
Z_div_ge0 [in Z_div_ge0]
Z_as_Int.i2z_opp [in i2z_opp]
Z_mod_same [in Z_mod_same]
Z_mult_quot_le [in Z_mult_quot_le]
Z_modulo_2 [in Z_modulo_2]
Z_to_binary_Sn [in Z_to_binary_Sn]
Z_mod_zero_opp_r [in Z_mod_zero_opp_r]
Z_div_mod_full [in Z_div_mod_full]
Z_mult_quot_ge [in Z_mult_quot_ge]
Z.abs_eq [in abs_eq]
Z.abs_neq [in abs_neq]
Z.add_diag [in add_diag]
Z.add_succ_l [in add_succ_l]
Z.add_reg_l [in add_reg_l]
Z.add_compare_mono_l [in add_compare_mono_l]
Z.add_0_l [in add_0_l]
Z.bi_induction [in bi_induction]
Z.compare_lt_iff [in compare_lt_iff]
Z.compare_antisym [in compare_antisym]
Z.compare_le_iff [in compare_le_iff]
Z.compare_eq_iff [in compare_eq_iff]
Z.compare_sub [in compare_sub]
Z.compare_opp [in compare_opp]
Z.div_eucl_eq [in div_eucl_eq]
Z.div_mod [in div_mod]
Z.div2_spec [in div2_spec]
Z.double_spec [in double_spec]
Z.eqb_eq [in eqb_eq]
Z.even_spec [in even_spec]
Z.gcd_nonneg [in gcd_nonneg]
Z.gcd_greatest [in gcd_greatest]
Z.gcd_divide_r [in gcd_divide_r]
Z.gcd_divide_l [in gcd_divide_l]
Z.geb_spec [in geb_spec]
Z.geb_leb [in geb_leb]
Z.geb_le [in geb_le]
Z.ge_le [in ge_le]
Z.ge_le_iff [in ge_le_iff]
Z.ggcd_correct_divisors [in ggcd_correct_divisors]
Z.ggcd_opp [in ggcd_opp]
Z.ggcd_gcd [in ggcd_gcd]
Z.gtb_spec [in gtb_spec]
Z.gtb_lt [in gtb_lt]
Z.gtb_ltb [in gtb_ltb]
Z.gt_lt [in gt_lt]
Z.gt_lt_iff [in gt_lt_iff]
Z.land_spec [in land_spec]
Z.ldiff_spec [in ldiff_spec]
Z.leb_le [in leb_le]
Z.le_ge [in le_ge]
Z.log2_spec [in log2_spec]
Z.log2_nonpos [in log2_nonpos]
Z.lor_spec [in lor_spec]
Z.ltb_lt [in ltb_lt]
Z.lt_succ_r [in lt_succ_r]
Z.lt_gt [in lt_gt]
Z.lxor_spec [in lxor_spec]
Z.max_r [in max_r]
Z.max_l [in max_l]
Z.min_r [in min_r]
Z.min_l [in min_l]
Z.mod_neg_bound [in mod_neg_bound]
Z.mod_pos_bound [in mod_pos_bound]
Z.mul_reg_l [in mul_reg_l]
Z.mul_succ_l [in mul_succ_l]
Z.mul_reg_r [in mul_reg_r]
Z.mul_0_l [in mul_0_l]
Z.odd_spec [in odd_spec]
Z.one_succ [in one_succ]
Z.opp_eq_mul_m1 [in opp_eq_mul_m1]
Z.opp_succ [in opp_succ]
Z.opp_0 [in opp_0]
Z.peano_ind [in peano_ind]
Z.pos_sub_gt [in pos_sub_gt]
Z.pos_div_eucl_bound [in pos_div_eucl_bound]
Z.pos_sub_spec [in pos_sub_spec]
Z.pos_sub_opp [in pos_sub_opp]
Z.pos_sub_lt [in pos_sub_lt]
Z.pos_div_eucl_eq [in pos_div_eucl_eq]
Z.pos_sub_diag [in pos_sub_diag]
Z.pos_sub_discr [in pos_sub_discr]
Z.pow_0_r [in pow_0_r]
Z.pow_pos_fold [in pow_pos_fold]
Z.pow_succ_r [in pow_succ_r]
Z.pow_neg_r [in pow_neg_r]
Z.pred_double_spec [in pred_double_spec]
Z.pred_succ [in pred_succ]
Z.Private_BootStrap.add_opp_diag_l [in add_opp_diag_l]
Z.Private_BootStrap.divide_Zpos_Zneg_l [in divide_Zpos_Zneg_l]
Z.Private_BootStrap.mul_1_r [in mul_1_r]
Z.Private_BootStrap.add_opp_diag_r [in add_opp_diag_r]
Z.Private_BootStrap.mul_add_distr_l [in mul_add_distr_l]
Z.Private_BootStrap.mul_add_distr_pos [in mul_add_distr_pos]
Z.Private_BootStrap.add_0_r [in add_0_r]
Z.Private_BootStrap.testbit_of_N [in testbit_of_N]
Z.Private_BootStrap.sub_succ_l [in sub_succ_l]
Z.Private_BootStrap.divide_Zpos_Zneg_r [in divide_Zpos_Zneg_r]
Z.Private_BootStrap.mul_opp_r [in mul_opp_r]
Z.Private_BootStrap.add_assoc [in add_assoc]
Z.Private_BootStrap.add_comm [in add_comm]
Z.Private_BootStrap.testbit_Zneg [in testbit_Zneg]
Z.Private_BootStrap.testbit_of_N' [in testbit_of_N']
Z.Private_BootStrap.mul_1_l [in mul_1_l]
Z.Private_BootStrap.mul_add_distr_r [in mul_add_distr_r]
Z.Private_BootStrap.pos_sub_add [in pos_sub_add]
Z.Private_BootStrap.mul_comm [in mul_comm]
Z.Private_BootStrap.mul_opp_comm [in mul_opp_comm]
Z.Private_BootStrap.mul_opp_l [in mul_opp_l]
Z.Private_BootStrap.mul_assoc [in mul_assoc]
Z.Private_BootStrap.mul_opp_opp [in mul_opp_opp]
Z.Private_BootStrap.opp_inj [in opp_inj]
Z.Private_BootStrap.divide_Zpos [in divide_Zpos]
Z.Private_BootStrap.testbit_Zpos [in testbit_Zpos]
Z.Private_BootStrap.opp_add_distr [in opp_add_distr]
Z.quotrem_eq [in quotrem_eq]
Z.quot_rem [in quot_rem]
Z.quot_rem' [in quot_rem']
Z.rem_opp_r' [in rem_opp_r']
Z.rem_opp_l [in rem_opp_l]
Z.rem_bound_pos [in rem_bound_pos]
Z.rem_opp_r [in rem_opp_r]
Z.rem_opp_l' [in rem_opp_l']
Z.sgn_pos [in sgn_pos]
Z.sgn_null [in sgn_null]
Z.sgn_neg [in sgn_neg]
Z.shiftl_spec_low [in shiftl_spec_low]
Z.shiftl_spec_high [in shiftl_spec_high]
Z.shiftr_spec_aux [in shiftr_spec_aux]
Z.shiftr_spec [in shiftr_spec]
Z.sqrtrem_sqrt [in sqrtrem_sqrt]
Z.sqrtrem_spec [in sqrtrem_spec]
Z.sqrt_spec [in sqrt_spec]
Z.sqrt_neg [in sqrt_neg]
Z.square_spec [in square_spec]
Z.sub_succ_r [in sub_succ_r]
Z.sub_0_r [in sub_0_r]
Z.succ_pred [in succ_pred]
Z.succ_double_spec [in succ_double_spec]
Z.testbit_even_0 [in testbit_even_0]
Z.testbit_neg_r [in testbit_neg_r]
Z.testbit_even_succ [in testbit_even_succ]
Z.testbit_0_l [in testbit_0_l]
Z.testbit_odd_0 [in testbit_odd_0]
Z.testbit_odd_succ [in testbit_odd_succ]
Z.two_succ [in two_succ]
Z2Nat.id [in id]
Z2Nat.inj [in inj]
Z2Nat.inj_max [in inj_max]
Z2Nat.inj_lt [in inj_lt]
Z2Nat.inj_pos [in inj_pos]
Z2Nat.inj_mul [in inj_mul]
Z2Nat.inj_iff [in inj_iff]
Z2Nat.inj_0 [in inj_0]
Z2Nat.inj_add [in inj_add]
Z2Nat.inj_compare [in inj_compare]
Z2Nat.inj_sub [in inj_sub]
Z2Nat.inj_min [in inj_min]
Z2Nat.inj_le [in inj_le]
Z2Nat.inj_neg [in inj_neg]
Z2Nat.inj_pred [in inj_pred]
Z2Nat.inj_succ [in inj_succ]
Z2N.id [in id]
Z2N.inj [in inj]
Z2N.inj_max [in inj_max]
Z2N.inj_lt [in inj_lt]
Z2N.inj_pos [in inj_pos]
Z2N.inj_mul [in inj_mul]
Z2N.inj_mod [in inj_mod]
Z2N.inj_iff [in inj_iff]
Z2N.inj_quot [in inj_quot]
Z2N.inj_0 [in inj_0]
Z2N.inj_add [in inj_add]
Z2N.inj_div2 [in inj_div2]
Z2N.inj_compare [in inj_compare]
Z2N.inj_sub [in inj_sub]
Z2N.inj_testbit [in inj_testbit]
Z2N.inj_min [in inj_min]
Z2N.inj_quot2 [in inj_quot2]
Z2N.inj_le [in inj_le]
Z2N.inj_neg [in inj_neg]
Z2N.inj_pred [in inj_pred]
Z2N.inj_succ [in inj_succ]
Z2N.inj_div [in inj_div]
Z2N.inj_rem [in inj_rem]
Z2N.inj_pow [in inj_pow]
Z2Pos.id [in id]
Z2Pos.inj [in inj]
Z2Pos.inj_max [in inj_max]
Z2Pos.inj_succ_double [in inj_succ_double]
Z2Pos.inj_sqrt [in inj_sqrt]
Z2Pos.inj_mul [in inj_mul]
Z2Pos.inj_double [in inj_double]
Z2Pos.inj_iff [in inj_iff]
Z2Pos.inj_leb [in inj_leb]
Z2Pos.inj_add [in inj_add]
Z2Pos.inj_gcd [in inj_gcd]
Z2Pos.inj_compare [in inj_compare]
Z2Pos.inj_sub [in inj_sub]
Z2Pos.inj_1 [in inj_1]
Z2Pos.inj_min [in inj_min]
Z2Pos.inj_ltb [in inj_ltb]
Z2Pos.inj_pred [in inj_pred]
Z2Pos.inj_succ [in inj_succ]
Z2Pos.inj_pow [in inj_pow]
Z2Pos.inj_eqb [in inj_eqb]
Z2Pos.inj_pow_pos [in inj_pow_pos]
Z2Pos.to_pos_nonpos [in to_pos_nonpos]



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)