Z
Z [module, in Z]
Z [inductive, in Z]
Z [abbreviation, in Z]
Z [module, in Z]
Z [module, in Z]
Zabs [abbreviation, in Zabs]
Zabs [library]
Zabs_N [abbreviation, in Zabs_N]
Zabs_pos [abbreviation, in Zabs_pos]
Zabs_triangle [abbreviation, in Zabs_triangle]
Zabs_nat_Zplus [abbreviation, in Zabs_nat_Zplus]
Zabs_Zsgn [abbreviation, in Zabs_Zsgn]
Zabs_N_mult_abs [abbreviation, in Zabs_N_mult_abs]
Zabs_N_succ_abs [abbreviation, in Zabs_N_succ_abs]
Zabs_nat_N [lemma, in Zabs_nat_N]
Zabs_N_plus [abbreviation, in Zabs_N_plus]
Zabs_involutive [abbreviation, in Zabs_involutive]
Zabs_Qabs [lemma, in Zabs_Qabs]
Zabs_spec [lemma, in Zabs_spec]
Zabs_N_succ [abbreviation, in Zabs_N_succ]
Zabs_non_eq [abbreviation, in Zabs_non_eq]
Zabs_non_eq [abbreviation, in Zabs_non_eq]
Zabs_of_N [abbreviation, in Zabs_of_N]
Zabs_nat_Zsucc [abbreviation, in Zabs_nat_Zsucc]
Zabs_Zopp [abbreviation, in Zabs_Zopp]
Zabs_intro [lemma, in Zabs_intro]
Zabs_ind [lemma, in Zabs_ind]
Zabs_nat_Z_of_nat [abbreviation, in Zabs_nat_Z_of_nat]
Zabs_nat_mult [abbreviation, in Zabs_nat_mult]
Zabs_Zmult [abbreviation, in Zabs_Zmult]
Zabs_nat_lt [lemma, in Zabs_nat_lt]
Zabs_nat_compare [abbreviation, in Zabs_nat_compare]
Zabs_dec [definition, in Zabs_dec]
Zabs_nat_Zminus [abbreviation, in Zabs_nat_Zminus]
Zabs_square [abbreviation, in Zabs_square]
Zabs_N_mult [abbreviation, in Zabs_N_mult]
Zabs_nat [abbreviation, in Zabs_nat]
Zabs_nat_le [lemma, in Zabs_nat_le]
Zabs_eq_case [abbreviation, in Zabs_eq_case]
Zabs_N_plus_abs [abbreviation, in Zabs_N_plus_abs]
Zabs_N_nat [lemma, in Zabs_N_nat]
Zabs_eq [abbreviation, in Zabs_eq]
Zabs_eq [abbreviation, in Zabs_eq]
Zabs2N [module, in Zabs2N]
Zabs2Nat [module, in Zabs2Nat]
Zabs2Nat.abs_nat_spec [lemma, in abs_nat_spec]
Zabs2Nat.abs_nat_nonneg [lemma, in abs_nat_nonneg]
Zabs2Nat.id [lemma, in id]
Zabs2Nat.id_abs [lemma, in id_abs]
Zabs2Nat.inj_succ_abs [lemma, in inj_succ_abs]
Zabs2Nat.inj_max [lemma, in inj_max]
Zabs2Nat.inj_lt [lemma, in inj_lt]
Zabs2Nat.inj_mul_abs [lemma, in inj_mul_abs]
Zabs2Nat.inj_pos [lemma, in inj_pos]
Zabs2Nat.inj_mul [lemma, in inj_mul]
Zabs2Nat.inj_0 [lemma, in inj_0]
Zabs2Nat.inj_add [lemma, in inj_add]
Zabs2Nat.inj_compare [lemma, in inj_compare]
Zabs2Nat.inj_sub [lemma, in inj_sub]
Zabs2Nat.inj_min [lemma, in inj_min]
Zabs2Nat.inj_add_abs [lemma, in inj_add_abs]
Zabs2Nat.inj_le [lemma, in inj_le]
Zabs2Nat.inj_neg [lemma, in inj_neg]
Zabs2Nat.inj_pred [lemma, in inj_pred]
Zabs2Nat.inj_succ [lemma, in inj_succ]
Zabs2N.abs_N_nonneg [lemma, in abs_N_nonneg]
Zabs2N.abs_N_spec [lemma, in abs_N_spec]
Zabs2N.id [lemma, in id]
Zabs2N.id_abs [lemma, in id_abs]
Zabs2N.inj_succ_abs [lemma, in inj_succ_abs]
Zabs2N.inj_max [lemma, in inj_max]
Zabs2N.inj_lt [lemma, in inj_lt]
Zabs2N.inj_mul_abs [lemma, in inj_mul_abs]
Zabs2N.inj_pos [lemma, in inj_pos]
Zabs2N.inj_mul [lemma, in inj_mul]
Zabs2N.inj_quot [lemma, in inj_quot]
Zabs2N.inj_0 [lemma, in inj_0]
Zabs2N.inj_add [lemma, in inj_add]
Zabs2N.inj_compare [lemma, in inj_compare]
Zabs2N.inj_sub [lemma, in inj_sub]
Zabs2N.inj_min [lemma, in inj_min]
Zabs2N.inj_opp [lemma, in inj_opp]
Zabs2N.inj_add_abs [lemma, in inj_add_abs]
Zabs2N.inj_le [lemma, in inj_le]
Zabs2N.inj_neg [lemma, in inj_neg]
Zabs2N.inj_pred [lemma, in inj_pred]
Zabs2N.inj_succ [lemma, in inj_succ]
Zabs2N.inj_rem [lemma, in inj_rem]
Zabs2N.inj_pow [lemma, in inj_pow]
ZAdd [library]
ZAddOrder [library]
ZAddOrderProp [module, in ZAddOrderProp]
ZAddOrderProp.add_neg_nonpos [lemma, in add_neg_nonpos]
ZAddOrderProp.add_nonpos_neg [lemma, in add_nonpos_neg]
ZAddOrderProp.add_nonpos_nonpos [lemma, in add_nonpos_nonpos]
ZAddOrderProp.add_neg_neg [lemma, in add_neg_neg]
ZAddOrderProp.le_add_le_sub_r [lemma, in le_add_le_sub_r]
ZAddOrderProp.le_sub_nonneg [lemma, in le_sub_nonneg]
ZAddOrderProp.le_sub_le_add [lemma, in le_sub_le_add]
ZAddOrderProp.le_sub_le_add_l [lemma, in le_sub_le_add_l]
ZAddOrderProp.le_sub_0 [lemma, in le_sub_0]
ZAddOrderProp.le_sub_le_add_r [lemma, in le_sub_le_add_r]
ZAddOrderProp.le_lt_sub_lt [lemma, in le_lt_sub_lt]
ZAddOrderProp.le_le_sub_lt [lemma, in le_le_sub_lt]
ZAddOrderProp.le_0_sub [lemma, in le_0_sub]
ZAddOrderProp.le_add_le_sub_l [lemma, in le_add_le_sub_l]
ZAddOrderProp.lt_sub_lt_add_r [lemma, in lt_sub_lt_add_r]
ZAddOrderProp.lt_sub_pos [lemma, in lt_sub_pos]
ZAddOrderProp.lt_add_lt_sub_r [lemma, in lt_add_lt_sub_r]
ZAddOrderProp.lt_add_lt_sub_l [lemma, in lt_add_lt_sub_l]
ZAddOrderProp.lt_le_sub_lt [lemma, in lt_le_sub_lt]
ZAddOrderProp.lt_sub_lt_add [lemma, in lt_sub_lt_add]
ZAddOrderProp.lt_m1_0 [lemma, in lt_m1_0]
ZAddOrderProp.lt_sub_lt_add_l [lemma, in lt_sub_lt_add_l]
ZAddOrderProp.lt_sub_0 [lemma, in lt_sub_0]
ZAddOrderProp.lt_0_sub [lemma, in lt_0_sub]
ZAddOrderProp.opp_neg_pos [lemma, in opp_neg_pos]
ZAddOrderProp.opp_nonpos_nonneg [lemma, in opp_nonpos_nonneg]
ZAddOrderProp.opp_pos_neg [lemma, in opp_pos_neg]
ZAddOrderProp.opp_lt_mono [lemma, in opp_lt_mono]
ZAddOrderProp.opp_nonneg_nonpos [lemma, in opp_nonneg_nonpos]
ZAddOrderProp.opp_le_mono [lemma, in opp_le_mono]
ZAddOrderProp.PosNeg [section, in PosNeg]
ZAddOrderProp.PosNeg.P [variable, in P]
ZAddOrderProp.PosNeg.P_wd [variable, in P_wd]
ZAddOrderProp.sub_le_mono_l [lemma, in sub_le_mono_l]
ZAddOrderProp.sub_lt_mono_l [lemma, in sub_lt_mono_l]
ZAddOrderProp.sub_nonneg_cases [lemma, in sub_nonneg_cases]
ZAddOrderProp.sub_le_mono_r [lemma, in sub_le_mono_r]
ZAddOrderProp.sub_pos [abbreviation, in sub_pos]
ZAddOrderProp.sub_lt_mono_r [lemma, in sub_lt_mono_r]
ZAddOrderProp.sub_le_cases [lemma, in sub_le_cases]
ZAddOrderProp.sub_nonneg [abbreviation, in sub_nonneg]
ZAddOrderProp.sub_neg_cases [lemma, in sub_neg_cases]
ZAddOrderProp.sub_neg [abbreviation, in sub_neg]
ZAddOrderProp.sub_le_mono [lemma, in sub_le_mono]
ZAddOrderProp.sub_lt_mono [lemma, in sub_lt_mono]
ZAddOrderProp.sub_nonpos [abbreviation, in sub_nonpos]
ZAddOrderProp.sub_pos_cases [lemma, in sub_pos_cases]
ZAddOrderProp.sub_lt_cases [lemma, in sub_lt_cases]
ZAddOrderProp.sub_lt_le_mono [lemma, in sub_lt_le_mono]
ZAddOrderProp.sub_nonpos_cases [lemma, in sub_nonpos_cases]
ZAddOrderProp.sub_le_lt_mono [lemma, in sub_le_lt_mono]
ZAddOrderProp.zero_pos_neg [lemma, in zero_pos_neg]
ZAddProp [module, in ZAddProp]
ZAddProp.add_pred_r [lemma, in add_pred_r]
ZAddProp.add_simpl_r [lemma, in add_simpl_r]
ZAddProp.add_opp_diag_l [lemma, in add_opp_diag_l]
ZAddProp.add_sub_assoc [lemma, in add_sub_assoc]
ZAddProp.add_pred_l [lemma, in add_pred_l]
ZAddProp.add_move_l [lemma, in add_move_l]
ZAddProp.add_opp_diag_r [lemma, in add_opp_diag_r]
ZAddProp.add_move_0_l [lemma, in add_move_0_l]
ZAddProp.add_add_simpl_r_l [lemma, in add_add_simpl_r_l]
ZAddProp.add_add_simpl_l_r [lemma, in add_add_simpl_l_r]
ZAddProp.add_add_simpl_l_l [lemma, in add_add_simpl_l_l]
ZAddProp.add_sub_swap [lemma, in add_sub_swap]
ZAddProp.add_move_0_r [lemma, in add_move_0_r]
ZAddProp.add_add_simpl_r_r [lemma, in add_add_simpl_r_r]
ZAddProp.add_move_r [lemma, in add_move_r]
ZAddProp.add_simpl_l [lemma, in add_simpl_l]
ZAddProp.add_opp_r [lemma, in add_opp_r]
ZAddProp.add_opp_l [lemma, in add_opp_l]
ZAddProp.eq_opp_r [lemma, in eq_opp_r]
ZAddProp.eq_opp_l [lemma, in eq_opp_l]
ZAddProp.opp_inj_wd [lemma, in opp_inj_wd]
ZAddProp.opp_involutive [lemma, in opp_involutive]
ZAddProp.opp_sub_distr [lemma, in opp_sub_distr]
ZAddProp.opp_pred [lemma, in opp_pred]
ZAddProp.opp_inj [lemma, in opp_inj]
ZAddProp.opp_add_distr [lemma, in opp_add_distr]
ZAddProp.sub_add_simpl_r_l [lemma, in sub_add_simpl_r_l]
ZAddProp.sub_add_simpl_r_r [lemma, in sub_add_simpl_r_r]
ZAddProp.sub_sub_distr [lemma, in sub_sub_distr]
ZAddProp.sub_cancel_r [lemma, in sub_cancel_r]
ZAddProp.sub_move_0_r [lemma, in sub_move_0_r]
ZAddProp.sub_0_l [lemma, in sub_0_l]
ZAddProp.sub_move_0_l [lemma, in sub_move_0_l]
ZAddProp.sub_move_l [lemma, in sub_move_l]
ZAddProp.sub_pred_l [lemma, in sub_pred_l]
ZAddProp.sub_succ_l [lemma, in sub_succ_l]
ZAddProp.sub_simpl_r [lemma, in sub_simpl_r]
ZAddProp.sub_add [lemma, in sub_add]
ZAddProp.sub_diag [lemma, in sub_diag]
ZAddProp.sub_move_r [lemma, in sub_move_r]
ZAddProp.sub_pred_r [lemma, in sub_pred_r]
ZAddProp.sub_simpl_l [lemma, in sub_simpl_l]
ZAddProp.sub_opp_r [lemma, in sub_opp_r]
ZAddProp.sub_cancel_l [lemma, in sub_cancel_l]
ZAddProp.sub_opp_l [lemma, in sub_opp_l]
ZAddProp.sub_add_distr [lemma, in sub_add_distr]
ZArith [library]
ZArith_dec [library]
ZArith_base [library]
ZAxiom [module, in ZAxiom]
ZAxioms [library]
ZAxiomsMiniSig [module, in ZAxiomsMiniSig]
ZAxiomsMiniSig' [module, in ZAxiomsMiniSig']
ZAxiomsSig [module, in ZAxiomsSig]
ZAxiomsSig' [module, in ZAxiomsSig']
ZAxiom.succ_pred [axiom, in succ_pred]
ZBase [library]
ZBaseProp [module, in ZBaseProp]
ZBaseProp.pred_inj_wd [lemma, in pred_inj_wd]
ZBaseProp.pred_inj [lemma, in pred_inj]
ZBaseProp.succ_m1 [lemma, in succ_m1]
ZBinary [library]
ZBits [library]
ZBitsProp [module, in ZBitsProp]
ZBitsProp.add_carry_bits_aux [lemma, in add_carry_bits_aux]
ZBitsProp.add_bit0 [lemma, in add_bit0]
ZBitsProp.add_bit1 [lemma, in add_bit1]
ZBitsProp.add_nocarry_mod_lt_pow2 [lemma, in add_nocarry_mod_lt_pow2]
ZBitsProp.add_b2z_double_div2 [lemma, in add_b2z_double_div2]
ZBitsProp.add_carry_div2 [lemma, in add_carry_div2]
ZBitsProp.add_nocarry_lxor [lemma, in add_nocarry_lxor]
ZBitsProp.add_lnot_diag [lemma, in add_lnot_diag]
ZBitsProp.add_b2z_double_bit0 [lemma, in add_b2z_double_bit0]
ZBitsProp.add_nocarry_lt_pow2 [lemma, in add_nocarry_lt_pow2]
ZBitsProp.add_carry_bits [lemma, in add_carry_bits]
ZBitsProp.add3_bits_div2 [lemma, in add3_bits_div2]
ZBitsProp.add3_bit0 [lemma, in add3_bit0]
ZBitsProp.are_bits [lemma, in are_bits]
ZBitsProp.bits_iff_nonneg' [lemma, in bits_iff_nonneg']
ZBitsProp.bits_above_log2 [lemma, in bits_above_log2]
ZBitsProp.bits_iff_neg' [lemma, in bits_iff_neg']
ZBitsProp.bits_iff_nonneg [lemma, in bits_iff_nonneg]
ZBitsProp.bits_0 [lemma, in bits_0]
ZBitsProp.bits_above_log2_neg [lemma, in bits_above_log2_neg]
ZBitsProp.bits_iff_neg_ex [lemma, in bits_iff_neg_ex]
ZBitsProp.bits_m1 [lemma, in bits_m1]
ZBitsProp.bits_inj_0 [lemma, in bits_inj_0]
ZBitsProp.bits_iff_neg [lemma, in bits_iff_neg]
ZBitsProp.bits_inj_iff [lemma, in bits_inj_iff]
ZBitsProp.bits_inj [lemma, in bits_inj]
ZBitsProp.bits_inj_iff' [lemma, in bits_inj_iff']
ZBitsProp.bits_inj' [lemma, in bits_inj']
ZBitsProp.bits_iff_nonneg_ex [lemma, in bits_iff_nonneg_ex]
ZBitsProp.bits_opp [lemma, in bits_opp]
ZBitsProp.bit_log2 [lemma, in bit_log2]
ZBitsProp.bit_log2_neg [lemma, in bit_log2_neg]
ZBitsProp.bit0_eqb [lemma, in bit0_eqb]
ZBitsProp.bit0_odd [lemma, in bit0_odd]
ZBitsProp.bit0_mod [lemma, in bit0_mod]
ZBitsProp.b2z [definition, in b2z]
ZBitsProp.b2z_wd [instance, in b2z_wd]
ZBitsProp.b2z_bit0 [lemma, in b2z_bit0]
ZBitsProp.b2z_inj [lemma, in b2z_inj]
ZBitsProp.b2z_div2 [lemma, in b2z_div2]
ZBitsProp.clearbit [definition, in clearbit]
ZBitsProp.clearbit_spec' [lemma, in clearbit_spec']
ZBitsProp.clearbit_iff [lemma, in clearbit_iff]
ZBitsProp.clearbit_eq [lemma, in clearbit_eq]
ZBitsProp.clearbit_neq [lemma, in clearbit_neq]
ZBitsProp.clearbit_eqb [lemma, in clearbit_eqb]
ZBitsProp.clearbit_wd [instance, in clearbit_wd]
ZBitsProp.div_pow2_bits [lemma, in div_pow2_bits]
ZBitsProp.div2_nonneg [lemma, in div2_nonneg]
ZBitsProp.div2_neg [lemma, in div2_neg]
ZBitsProp.div2_wd [instance, in div2_wd]
ZBitsProp.div2_div [lemma, in div2_div]
ZBitsProp.div2_bits [lemma, in div2_bits]
ZBitsProp.div2_odd [lemma, in div2_odd]
ZBitsProp.double_bits_succ [lemma, in double_bits_succ]
ZBitsProp.double_bits [lemma, in double_bits]
ZBitsProp.eqf [definition, in eqf]
ZBitsProp.eqf_equiv [instance, in eqf_equiv]
ZBitsProp.exists_div2 [lemma, in exists_div2]
ZBitsProp.land_comm [lemma, in land_comm]
ZBitsProp.land_assoc [lemma, in land_assoc]
ZBitsProp.land_0_l [lemma, in land_0_l]
ZBitsProp.land_wd [instance, in land_wd]
ZBitsProp.land_m1_l [lemma, in land_m1_l]
ZBitsProp.land_ones_low [lemma, in land_ones_low]
ZBitsProp.land_ldiff [lemma, in land_ldiff]
ZBitsProp.land_lnot_diag [lemma, in land_lnot_diag]
ZBitsProp.land_neg [lemma, in land_neg]
ZBitsProp.land_lor_distr_r [lemma, in land_lor_distr_r]
ZBitsProp.land_ones [lemma, in land_ones]
ZBitsProp.land_diag [lemma, in land_diag]
ZBitsProp.land_m1_r [lemma, in land_m1_r]
ZBitsProp.land_0_r [lemma, in land_0_r]
ZBitsProp.land_lor_distr_l [lemma, in land_lor_distr_l]
ZBitsProp.land_nonneg [lemma, in land_nonneg]
ZBitsProp.ldiff_nonneg [lemma, in ldiff_nonneg]
ZBitsProp.ldiff_wd [instance, in ldiff_wd]
ZBitsProp.ldiff_neg [lemma, in ldiff_neg]
ZBitsProp.ldiff_ldiff_l [lemma, in ldiff_ldiff_l]
ZBitsProp.ldiff_ones_r_low [lemma, in ldiff_ones_r_low]
ZBitsProp.ldiff_ones_r [lemma, in ldiff_ones_r]
ZBitsProp.ldiff_ones_l_low [lemma, in ldiff_ones_l_low]
ZBitsProp.ldiff_diag [lemma, in ldiff_diag]
ZBitsProp.ldiff_le [lemma, in ldiff_le]
ZBitsProp.ldiff_0_l [lemma, in ldiff_0_l]
ZBitsProp.ldiff_m1_l [lemma, in ldiff_m1_l]
ZBitsProp.ldiff_land [lemma, in ldiff_land]
ZBitsProp.ldiff_0_r [lemma, in ldiff_0_r]
ZBitsProp.ldiff_m1_r [lemma, in ldiff_m1_r]
ZBitsProp.lnextcarry [abbreviation, in lnextcarry]
ZBitsProp.lnot [definition, in lnot]
ZBitsProp.lnot_m1 [lemma, in lnot_m1]
ZBitsProp.lnot_shiftr [lemma, in lnot_shiftr]
ZBitsProp.lnot_wd [instance, in lnot_wd]
ZBitsProp.lnot_lxor_l [lemma, in lnot_lxor_l]
ZBitsProp.lnot_0 [lemma, in lnot_0]
ZBitsProp.lnot_neg [lemma, in lnot_neg]
ZBitsProp.lnot_nonneg [lemma, in lnot_nonneg]
ZBitsProp.lnot_ldiff [lemma, in lnot_ldiff]
ZBitsProp.lnot_lor [lemma, in lnot_lor]
ZBitsProp.lnot_land [lemma, in lnot_land]
ZBitsProp.lnot_lxor_r [lemma, in lnot_lxor_r]
ZBitsProp.lnot_involutive [lemma, in lnot_involutive]
ZBitsProp.lnot_spec [lemma, in lnot_spec]
ZBitsProp.log2_lor [lemma, in log2_lor]
ZBitsProp.log2_shiftr [lemma, in log2_shiftr]
ZBitsProp.log2_lxor [lemma, in log2_lxor]
ZBitsProp.log2_bits_unique [lemma, in log2_bits_unique]
ZBitsProp.log2_shiftl [lemma, in log2_shiftl]
ZBitsProp.log2_land [lemma, in log2_land]
ZBitsProp.log2_shiftl' [lemma, in log2_shiftl']
ZBitsProp.lor_comm [lemma, in lor_comm]
ZBitsProp.lor_neg [lemma, in lor_neg]
ZBitsProp.lor_m1_r [lemma, in lor_m1_r]
ZBitsProp.lor_eq_0_iff [lemma, in lor_eq_0_iff]
ZBitsProp.lor_ldiff_and [lemma, in lor_ldiff_and]
ZBitsProp.lor_land_distr_r [lemma, in lor_land_distr_r]
ZBitsProp.lor_eq_0_l [lemma, in lor_eq_0_l]
ZBitsProp.lor_land_distr_l [lemma, in lor_land_distr_l]
ZBitsProp.lor_m1_l [lemma, in lor_m1_l]
ZBitsProp.lor_lnot_diag [lemma, in lor_lnot_diag]
ZBitsProp.lor_wd [instance, in lor_wd]
ZBitsProp.lor_0_r [lemma, in lor_0_r]
ZBitsProp.lor_ones_low [lemma, in lor_ones_low]
ZBitsProp.lor_assoc [lemma, in lor_assoc]
ZBitsProp.lor_diag [lemma, in lor_diag]
ZBitsProp.lor_0_l [lemma, in lor_0_l]
ZBitsProp.lor_nonneg [lemma, in lor_nonneg]
ZBitsProp.lxor_m1_r [lemma, in lxor_m1_r]
ZBitsProp.lxor_wd [instance, in lxor_wd]
ZBitsProp.lxor_lnot_lnot [lemma, in lxor_lnot_lnot]
ZBitsProp.lxor_0_r [lemma, in lxor_0_r]
ZBitsProp.lxor_0_l [lemma, in lxor_0_l]
ZBitsProp.lxor_lor [lemma, in lxor_lor]
ZBitsProp.lxor_m1_l [lemma, in lxor_m1_l]
ZBitsProp.lxor_eq_0_iff [lemma, in lxor_eq_0_iff]
ZBitsProp.lxor_comm [lemma, in lxor_comm]
ZBitsProp.lxor_nonneg [lemma, in lxor_nonneg]
ZBitsProp.lxor_assoc [lemma, in lxor_assoc]
ZBitsProp.lxor_eq [lemma, in lxor_eq]
ZBitsProp.lxor_nilpotent [lemma, in lxor_nilpotent]
ZBitsProp.lxor3 [abbreviation, in lxor3]
ZBitsProp.mod_pow2_bits_high [lemma, in mod_pow2_bits_high]
ZBitsProp.mod_pow2_bits_low [lemma, in mod_pow2_bits_low]
ZBitsProp.mul_pow2_bits_low [lemma, in mul_pow2_bits_low]
ZBitsProp.mul_pow2_bits_add [lemma, in mul_pow2_bits_add]
ZBitsProp.mul_pow2_bits [lemma, in mul_pow2_bits]
ZBitsProp.nextcarry [abbreviation, in nextcarry]
ZBitsProp.nocarry_equiv [lemma, in nocarry_equiv]
ZBitsProp.ones [definition, in ones]
ZBitsProp.ones_mod_pow2 [lemma, in ones_mod_pow2]
ZBitsProp.ones_div_pow2 [lemma, in ones_div_pow2]
ZBitsProp.ones_spec_iff [lemma, in ones_spec_iff]
ZBitsProp.ones_wd [instance, in ones_wd]
ZBitsProp.ones_add [lemma, in ones_add]
ZBitsProp.ones_equiv [lemma, in ones_equiv]
ZBitsProp.ones_spec_low [lemma, in ones_spec_low]
ZBitsProp.ones_spec_high [lemma, in ones_spec_high]
ZBitsProp.pow_div_l [lemma, in pow_div_l]
ZBitsProp.pow_sub_r [lemma, in pow_sub_r]
ZBitsProp.pow2_bits_eqb [lemma, in pow2_bits_eqb]
ZBitsProp.pow2_bits_false [lemma, in pow2_bits_false]
ZBitsProp.pow2_bits_true [lemma, in pow2_bits_true]
ZBitsProp.setbit [definition, in setbit]
ZBitsProp.setbit_neq [lemma, in setbit_neq]
ZBitsProp.setbit_eqb [lemma, in setbit_eqb]
ZBitsProp.setbit_eq [lemma, in setbit_eq]
ZBitsProp.setbit_spec' [lemma, in setbit_spec']
ZBitsProp.setbit_wd [instance, in setbit_wd]
ZBitsProp.setbit_iff [lemma, in setbit_iff]
ZBitsProp.shiftl_spec [lemma, in shiftl_spec]
ZBitsProp.shiftl_land [lemma, in shiftl_land]
ZBitsProp.shiftl_lxor [lemma, in shiftl_lxor]
ZBitsProp.shiftl_opp_r [lemma, in shiftl_opp_r]
ZBitsProp.shiftl_div_pow2 [lemma, in shiftl_div_pow2]
ZBitsProp.shiftl_1_l [lemma, in shiftl_1_l]
ZBitsProp.shiftl_nonneg [lemma, in shiftl_nonneg]
ZBitsProp.shiftl_wd [instance, in shiftl_wd]
ZBitsProp.shiftl_eq_0_iff [lemma, in shiftl_eq_0_iff]
ZBitsProp.shiftl_neg [lemma, in shiftl_neg]
ZBitsProp.shiftl_0_l [lemma, in shiftl_0_l]
ZBitsProp.shiftl_mul_pow2 [lemma, in shiftl_mul_pow2]
ZBitsProp.shiftl_ldiff [lemma, in shiftl_ldiff]
ZBitsProp.shiftl_0_r [lemma, in shiftl_0_r]
ZBitsProp.shiftl_shiftl [lemma, in shiftl_shiftl]
ZBitsProp.shiftl_spec_alt [lemma, in shiftl_spec_alt]
ZBitsProp.shiftl_lor [lemma, in shiftl_lor]
ZBitsProp.shiftr_div_pow2 [lemma, in shiftr_div_pow2]
ZBitsProp.shiftr_ldiff [lemma, in shiftr_ldiff]
ZBitsProp.shiftr_opp_r [lemma, in shiftr_opp_r]
ZBitsProp.shiftr_lxor [lemma, in shiftr_lxor]
ZBitsProp.shiftr_0_l [lemma, in shiftr_0_l]
ZBitsProp.shiftr_mul_pow2 [lemma, in shiftr_mul_pow2]
ZBitsProp.shiftr_neg [lemma, in shiftr_neg]
ZBitsProp.shiftr_shiftl_l [lemma, in shiftr_shiftl_l]
ZBitsProp.shiftr_nonneg [lemma, in shiftr_nonneg]
ZBitsProp.shiftr_wd [instance, in shiftr_wd]
ZBitsProp.shiftr_eq_0 [lemma, in shiftr_eq_0]
ZBitsProp.shiftr_shiftl_r [lemma, in shiftr_shiftl_r]
ZBitsProp.shiftr_land [lemma, in shiftr_land]
ZBitsProp.shiftr_lor [lemma, in shiftr_lor]
ZBitsProp.shiftr_0_r [lemma, in shiftr_0_r]
ZBitsProp.shiftr_shiftr [lemma, in shiftr_shiftr]
ZBitsProp.shiftr_eq_0_iff [lemma, in shiftr_eq_0_iff]
ZBitsProp.sub_nocarry_ldiff [lemma, in sub_nocarry_ldiff]
ZBitsProp.testbit_0_r [lemma, in testbit_0_r]
ZBitsProp.testbit_true [lemma, in testbit_true]
ZBitsProp.testbit_eqb [lemma, in testbit_eqb]
ZBitsProp.testbit_false [lemma, in testbit_false]
ZBitsProp.testbit_unique [lemma, in testbit_unique]
ZBitsProp.testbit_spec [lemma, in testbit_spec]
ZBitsProp.testbit_eqf [instance, in testbit_eqf]
ZBitsProp.testbit_spec' [lemma, in testbit_spec']
ZBitsProp.testbit_succ_r [lemma, in testbit_succ_r]
ZBitsProp.testbit_odd [lemma, in testbit_odd]
ZBitsProp.xor3 [abbreviation, in xor3]
_ === _ [notation, in ::x_'==='_x]
Zbool [library]
Zbounded_induction [lemma, in Zbounded_induction]
Zcase_sign [lemma, in Zcase_sign]
Zcompare [abbreviation, in Zcompare]
Zcompare [library]
Zcompare_refl [abbreviation, in Zcompare_refl]
Zcompare_Eq_iff_eq [abbreviation, in Zcompare_Eq_iff_eq]
Zcompare_mult_compat [lemma, in Zcompare_mult_compat]
Zcompare_Lt_trans [lemma, in Zcompare_Lt_trans]
Zcompare_spec [abbreviation, in Zcompare_spec]
Zcompare_rec [lemma, in Zcompare_rec]
Zcompare_Gt_not_Lt [lemma, in Zcompare_Gt_not_Lt]
Zcompare_opp [lemma, in Zcompare_opp]
Zcompare_Gt_trans [lemma, in Zcompare_Gt_trans]
Zcompare_succ_compat [lemma, in Zcompare_succ_compat]
Zcompare_eq_case [lemma, in Zcompare_eq_case]
Zcompare_succ_Gt [lemma, in Zcompare_succ_Gt]
Zcompare_elim [lemma, in Zcompare_elim]
Zcompare_Eq_eq [abbreviation, in Zcompare_Eq_eq]
Zcompare_Gt_spec [lemma, in Zcompare_Gt_spec]
Zcompare_antisym [lemma, in Zcompare_antisym]
Zcompare_Gt_Lt_antisym [lemma, in Zcompare_Gt_Lt_antisym]
Zcompare_gt [lemma, in Zcompare_gt]
Zcompare_rect [lemma, in Zcompare_rect]
Zcompare_plus_compat [lemma, in Zcompare_plus_compat]
Zcomplements [library]
ZC1 [abbreviation, in ZC1]
ZC2 [abbreviation, in ZC2]
ZC4 [lemma, in ZC4]
ZDecAxiomsSig [module, in ZDecAxiomsSig]
ZDecAxiomsSig' [module, in ZDecAxiomsSig']
zdigits [definition, in zdigits]
Zdigits [library]
ZDiv [module, in ZDiv]
Zdiv [abbreviation, in Zdiv]
Zdiv [library]
ZDivEucl [library]
ZDivFloor [library]
Zdivide [abbreviation, in Zdivide]
Zdivide_factor_r [abbreviation, in Zdivide_factor_r]
Zdivide_Zgcd [lemma, in Zdivide_Zgcd]
Zdivide_Zdiv_lt_pos [lemma, in Zdivide_Zdiv_lt_pos]
Zdivide_0 [abbreviation, in Zdivide_0]
Zdivide_factor_l [abbreviation, in Zdivide_factor_l]
Zdivide_intro [definition, in Zdivide_intro]
Zdivide_dec [lemma, in Zdivide_dec]
Zdivide_antisym [abbreviation, in Zdivide_antisym]
Zdivide_opp_l_rev [lemma, in Zdivide_opp_l_rev]
Zdivide_1 [abbreviation, in Zdivide_1]
Zdivide_trans [abbreviation, in Zdivide_trans]
Zdivide_Zdiv_eq_2 [lemma, in Zdivide_Zdiv_eq_2]
Zdivide_opp_r [lemma, in Zdivide_opp_r]
Zdivide_Zabs_l [lemma, in Zdivide_Zabs_l]
Zdivide_opp_l [lemma, in Zdivide_opp_l]
Zdivide_minus_l [abbreviation, in Zdivide_minus_l]
Zdivide_mult_l [abbreviation, in Zdivide_mult_l]
Zdivide_plus_r [abbreviation, in Zdivide_plus_r]
Zdivide_le [lemma, in Zdivide_le]
Zdivide_opp_r_rev [lemma, in Zdivide_opp_r_rev]
Zdivide_Zdiv_eq [lemma, in Zdivide_Zdiv_eq]
Zdivide_mod [lemma, in Zdivide_mod]
Zdivide_Zabs_inv_l [lemma, in Zdivide_Zabs_inv_l]
Zdivide_refl [abbreviation, in Zdivide_refl]
Zdivide_mult_r [abbreviation, in Zdivide_mult_r]
Zdivide_mod_minus [lemma, in Zdivide_mod_minus]
Zdivide_bounds [lemma, in Zdivide_bounds]
Zdivide_power_2 [lemma, in Zdivide_power_2]
ZDivProp [module, in ZDivProp]
ZDivProp.add_mod_idemp_r [lemma, in add_mod_idemp_r]
ZDivProp.add_mod_idemp_l [lemma, in add_mod_idemp_l]
ZDivProp.add_mod [lemma, in add_mod]
ZDivProp.div_mod_unique [lemma, in div_mod_unique]
ZDivProp.div_unique [lemma, in div_unique]
ZDivProp.div_small_iff [lemma, in div_small_iff]
ZDivProp.div_unique_neg [lemma, in div_unique_neg]
ZDivProp.div_mul_le [lemma, in div_mul_le]
ZDivProp.div_mul [lemma, in div_mul]
ZDivProp.div_0_l [lemma, in div_0_l]
ZDivProp.div_div [lemma, in div_div]
ZDivProp.div_add [lemma, in div_add]
ZDivProp.div_1_l [lemma, in div_1_l]
ZDivProp.div_opp_opp [lemma, in div_opp_opp]
ZDivProp.div_exact [lemma, in div_exact]
ZDivProp.div_le_mono [lemma, in div_le_mono]
ZDivProp.div_same [lemma, in div_same]
ZDivProp.div_pos [lemma, in div_pos]
ZDivProp.div_unique_exact [lemma, in div_unique_exact]
ZDivProp.div_mul_cancel_r [lemma, in div_mul_cancel_r]
ZDivProp.div_opp_l_nz [lemma, in div_opp_l_nz]
ZDivProp.div_le_compat_l [lemma, in div_le_compat_l]
ZDivProp.div_le_upper_bound [lemma, in div_le_upper_bound]
ZDivProp.div_lt [lemma, in div_lt]
ZDivProp.div_mul_cancel_l [lemma, in div_mul_cancel_l]
ZDivProp.div_le_lower_bound [lemma, in div_le_lower_bound]
ZDivProp.div_opp_l_z [lemma, in div_opp_l_z]
ZDivProp.div_small [lemma, in div_small]
ZDivProp.div_str_pos [lemma, in div_str_pos]
ZDivProp.div_1_r [lemma, in div_1_r]
ZDivProp.div_lt_upper_bound [lemma, in div_lt_upper_bound]
ZDivProp.div_unique_pos [lemma, in div_unique_pos]
ZDivProp.div_opp_r_nz [lemma, in div_opp_r_nz]
ZDivProp.div_opp_r_z [lemma, in div_opp_r_z]
ZDivProp.div_add_l [lemma, in div_add_l]
ZDivProp.mod_1_r [lemma, in mod_1_r]
ZDivProp.mod_small_iff [lemma, in mod_small_iff]
ZDivProp.mod_opp_r_nz [lemma, in mod_opp_r_nz]
ZDivProp.mod_opp_l_z [lemma, in mod_opp_l_z]
ZDivProp.mod_unique [lemma, in mod_unique]
ZDivProp.mod_opp_l_nz [lemma, in mod_opp_l_nz]
ZDivProp.mod_opp_r_z [lemma, in mod_opp_r_z]
ZDivProp.mod_le [lemma, in mod_le]
ZDivProp.mod_add [lemma, in mod_add]
ZDivProp.mod_small [lemma, in mod_small]
ZDivProp.mod_mod [lemma, in mod_mod]
ZDivProp.mod_sign [lemma, in mod_sign]
ZDivProp.mod_eq [lemma, in mod_eq]
ZDivProp.mod_bound_abs [lemma, in mod_bound_abs]
ZDivProp.mod_0_l [lemma, in mod_0_l]
ZDivProp.mod_opp_opp [lemma, in mod_opp_opp]
ZDivProp.mod_mul [lemma, in mod_mul]
ZDivProp.mod_sign_nz [lemma, in mod_sign_nz]
ZDivProp.mod_same [lemma, in mod_same]
ZDivProp.mod_unique_pos [lemma, in mod_unique_pos]
ZDivProp.mod_sign_mul [lemma, in mod_sign_mul]
ZDivProp.mod_unique_neg [lemma, in mod_unique_neg]
ZDivProp.mod_bound_or [lemma, in mod_bound_or]
ZDivProp.mod_1_l [lemma, in mod_1_l]
ZDivProp.mul_succ_div_gt [lemma, in mul_succ_div_gt]
ZDivProp.mul_mod [lemma, in mul_mod]
ZDivProp.mul_mod_distr_r [lemma, in mul_mod_distr_r]
ZDivProp.mul_mod_distr_l [lemma, in mul_mod_distr_l]
ZDivProp.mul_mod_idemp_r [lemma, in mul_mod_idemp_r]
ZDivProp.mul_succ_div_lt [lemma, in mul_succ_div_lt]
ZDivProp.mul_div_ge [lemma, in mul_div_ge]
ZDivProp.mul_mod_idemp_l [lemma, in mul_mod_idemp_l]
ZDivProp.mul_div_le [lemma, in mul_div_le]
ZDivProp.opp_mod_bound_or [lemma, in opp_mod_bound_or]
ZDivProp.Private_NZDiv [module, in ZDivProp.Private_NZDiv]
ZDivProp.rem_mul_r [lemma, in rem_mul_r]
ZDivSpecific [module, in ZDivSpecific]
ZDivSpecific.mod_neg_bound [axiom, in mod_neg_bound]
ZDivSpecific.mod_pos_bound [axiom, in mod_pos_bound]
ZDivTrunc [library]
Zdiv_eucl [abbreviation, in Zdiv_eucl]
Zdiv_Zdiv [lemma, in Zdiv_Zdiv]
Zdiv_gcd_zero [lemma, in Zdiv_gcd_zero]
Zdiv_rest_aux [definition, in Zdiv_rest_aux]
Zdiv_lt_upper_bound [lemma, in Zdiv_lt_upper_bound]
Zdiv_shift_r [lemma, in Zdiv_shift_r]
Zdiv_eucl_exist [lemma, in Zdiv_eucl_exist]
Zdiv_rest_correct2 [lemma, in Zdiv_rest_correct2]
Zdiv_1_l [lemma, in Zdiv_1_l]
Zdiv_eucl_eq [abbreviation, in Zdiv_eucl_eq]
Zdiv_rest [definition, in Zdiv_rest]
Zdiv_0_l [lemma, in Zdiv_0_l]
Zdiv_mod_unique [lemma, in Zdiv_mod_unique]
Zdiv_unique [lemma, in Zdiv_unique]
Zdiv_neg [lemma, in Zdiv_neg]
Zdiv_opp_opp [lemma, in Zdiv_opp_opp]
Zdiv_mult_le [lemma, in Zdiv_mult_le]
Zdiv_rest_ok [lemma, in Zdiv_rest_ok]
Zdiv_sgn [lemma, in Zdiv_sgn]
Zdiv_Qdiv [lemma, in Zdiv_Qdiv]
Zdiv_le_lower_bound [lemma, in Zdiv_le_lower_bound]
Zdiv_eucl_extended [lemma, in Zdiv_eucl_extended]
Zdiv_rest_proofs [inductive, in Zdiv_rest_proofs]
Zdiv_eucl_POS [abbreviation, in Zdiv_eucl_POS]
Zdiv_1_r [lemma, in Zdiv_1_r]
Zdiv_mult_cancel_r [definition, in Zdiv_mult_cancel_r]
Zdiv_mult_cancel_r [lemma, in Zdiv_mult_cancel_r]
Zdiv_mult_cancel_l [definition, in Zdiv_mult_cancel_l]
Zdiv_mult_cancel_l [lemma, in Zdiv_mult_cancel_l]
Zdiv_small [lemma, in Zdiv_small]
Zdiv_rest_correct [lemma, in Zdiv_rest_correct]
Zdiv_le_upper_bound [lemma, in Zdiv_le_upper_bound]
Zdiv_rest_proof [constructor, in Zdiv_rest_proof]
Zdiv_mod_unique_2 [lemma, in Zdiv_mod_unique_2]
Zdiv_unique_full [lemma, in Zdiv_unique_full]
Zdiv_le_compat_l [lemma, in Zdiv_le_compat_l]
Zdiv_rest_shiftr [lemma, in Zdiv_rest_shiftr]
Zdiv_0_r [lemma, in Zdiv_0_r]
Zdiv_rest_correct1 [lemma, in Zdiv_rest_correct1]
ZDiv' [module, in ZDiv']
Zdiv2 [abbreviation, in Zdiv2]
Zdiv2_div [lemma, in Zdiv2_div]
Zdiv2_odd_eqn [lemma, in Zdiv2_odd_eqn]
Zdiv2_two_power_nat [lemma, in Zdiv2_two_power_nat]
Zdouble [abbreviation, in Zdouble]
Zdouble_mult [abbreviation, in Zdouble_mult]
Zdouble_plus_one [abbreviation, in Zdouble_plus_one]
Zdouble_minus_one [abbreviation, in Zdouble_minus_one]
Zdouble_plus_one_mult [abbreviation, in Zdouble_plus_one_mult]
Zegal_left [lemma, in Zegal_left]
Zeq_bool_if [lemma, in Zeq_bool_if]
Zeq_plus_swap [lemma, in Zeq_plus_swap]
Zeq_is_eq_bool [lemma, in Zeq_is_eq_bool]
Zeq_le [abbreviation, in Zeq_le]
Zeq_bool_neq [lemma, in Zeq_bool_neq]
Zeq_bool_eq [lemma, in Zeq_bool_eq]
Zeq_minus [lemma, in Zeq_minus]
Zeq_bool [definition, in Zeq_bool]
zero [definition, in zero]
zero [definition, in zero]
zerob [definition, in zerob]
Zerob [library]
zerob_false_elim [lemma, in zerob_false_elim]
zerob_false_intro [lemma, in zerob_false_intro]
zerob_true_elim [lemma, in zerob_true_elim]
zerob_true_intro [lemma, in zerob_true_intro]
zerop [definition, in zerop]
zerop_bool [definition, in zerop_bool]
ZeroSuccPred [module, in ZeroSuccPred]
ZeroSuccPredNotation [module, in ZeroSuccPredNotation]
ZeroSuccPredNotation.P [abbreviation, in P]
ZeroSuccPredNotation.S [abbreviation, in S]
0 [notation, in ::'0']
ZeroSuccPred' [module, in ZeroSuccPred']
ZeroSuccPred.pred [axiom, in pred]
ZeroSuccPred.succ [axiom, in succ]
ZeroSuccPred.zero [axiom, in zero]
ZERO_le_N_digits [lemma, in ZERO_le_N_digits]
ZEuclid [module, in ZEuclid]
ZEuclid [module, in ZEuclid]
Zeuclid [library]
ZEuclidProp [module, in ZEuclidProp]
ZEuclidProp.add_mod_idemp_r [lemma, in add_mod_idemp_r]
ZEuclidProp.add_mod_idemp_l [lemma, in add_mod_idemp_l]
ZEuclidProp.add_mod [lemma, in add_mod]
ZEuclidProp.div_mod_unique [lemma, in div_mod_unique]
ZEuclidProp.div_unique [lemma, in div_unique]
ZEuclidProp.div_small_iff [lemma, in div_small_iff]
ZEuclidProp.div_mul_le [lemma, in div_mul_le]
ZEuclidProp.div_mul [lemma, in div_mul]
ZEuclidProp.div_0_l [lemma, in div_0_l]
ZEuclidProp.div_div [lemma, in div_div]
ZEuclidProp.div_add [lemma, in div_add]
ZEuclidProp.div_1_l [lemma, in div_1_l]
ZEuclidProp.div_opp_opp_z [lemma, in div_opp_opp_z]
ZEuclidProp.div_exact [lemma, in div_exact]
ZEuclidProp.div_le_mono [lemma, in div_le_mono]
ZEuclidProp.div_same [lemma, in div_same]
ZEuclidProp.div_pos [lemma, in div_pos]
ZEuclidProp.div_unique_exact [lemma, in div_unique_exact]
ZEuclidProp.div_mul_cancel_r [lemma, in div_mul_cancel_r]
ZEuclidProp.div_opp_l_nz [lemma, in div_opp_l_nz]
ZEuclidProp.div_le_compat_l [lemma, in div_le_compat_l]
ZEuclidProp.div_opp_r [lemma, in div_opp_r]
ZEuclidProp.div_le_upper_bound [lemma, in div_le_upper_bound]
ZEuclidProp.div_lt [lemma, in div_lt]
ZEuclidProp.div_mul_cancel_l [lemma, in div_mul_cancel_l]
ZEuclidProp.div_le_lower_bound [lemma, in div_le_lower_bound]
ZEuclidProp.div_opp_l_z [lemma, in div_opp_l_z]
ZEuclidProp.div_small [lemma, in div_small]
ZEuclidProp.div_str_pos [lemma, in div_str_pos]
ZEuclidProp.div_1_r [lemma, in div_1_r]
ZEuclidProp.div_lt_upper_bound [lemma, in div_lt_upper_bound]
ZEuclidProp.div_opp_opp_nz [lemma, in div_opp_opp_nz]
ZEuclidProp.div_add_l [lemma, in div_add_l]
ZEuclidProp.mod_1_r [lemma, in mod_1_r]
ZEuclidProp.mod_small_iff [lemma, in mod_small_iff]
ZEuclidProp.mod_opp_l_z [lemma, in mod_opp_l_z]
ZEuclidProp.mod_mul_r [lemma, in mod_mul_r]
ZEuclidProp.mod_unique [lemma, in mod_unique]
ZEuclidProp.mod_opp_l_nz [lemma, in mod_opp_l_nz]
ZEuclidProp.mod_le [lemma, in mod_le]
ZEuclidProp.mod_add [lemma, in mod_add]
ZEuclidProp.mod_small [lemma, in mod_small]
ZEuclidProp.mod_mod [lemma, in mod_mod]
ZEuclidProp.mod_divides [lemma, in mod_divides]
ZEuclidProp.mod_eq [lemma, in mod_eq]
ZEuclidProp.mod_opp_r [lemma, in mod_opp_r]
ZEuclidProp.mod_0_l [lemma, in mod_0_l]
ZEuclidProp.mod_mul [lemma, in mod_mul]
ZEuclidProp.mod_opp_opp_nz [lemma, in mod_opp_opp_nz]
ZEuclidProp.mod_same [lemma, in mod_same]
ZEuclidProp.mod_opp_opp_z [lemma, in mod_opp_opp_z]
ZEuclidProp.mod_1_l [lemma, in mod_1_l]
ZEuclidProp.mul_succ_div_gt [lemma, in mul_succ_div_gt]
ZEuclidProp.mul_mod [lemma, in mul_mod]
ZEuclidProp.mul_mod_distr_r [lemma, in mul_mod_distr_r]
ZEuclidProp.mul_mod_distr_l [lemma, in mul_mod_distr_l]
ZEuclidProp.mul_mod_idemp_r [lemma, in mul_mod_idemp_r]
ZEuclidProp.mul_mod_idemp_l [lemma, in mul_mod_idemp_l]
ZEuclidProp.mul_pred_div_gt [lemma, in mul_pred_div_gt]
ZEuclidProp.mul_div_le [lemma, in mul_div_le]
ZEuclidProp.Private_NZDiv [module, in ZEuclidProp.Private_NZDiv]
ZEuclid' [module, in ZEuclid']
ZEuclid.div [definition, in div]
ZEuclid.div_wd [instance, in div_wd]
ZEuclid.div_mod [lemma, in div_mod]
ZEuclid.modulo [definition, in modulo]
ZEuclid.mod_bound_pos [lemma, in mod_bound_pos]
ZEuclid.mod_always_pos [lemma, in mod_always_pos]
ZEuclid.mod_wd [instance, in mod_wd]
Zeven [definition, in Zeven]
Zeven [library]
Zeven_odd_bool [lemma, in Zeven_odd_bool]
Zeven_odd_bool [definition, in Zeven_odd_bool]
Zeven_bit_value [lemma, in Zeven_bit_value]
Zeven_odd_dec [definition, in Zeven_odd_dec]
Zeven_dec [definition, in Zeven_dec]
Zeven_mult_Zeven_l [lemma, in Zeven_mult_Zeven_l]
Zeven_pred [lemma, in Zeven_pred]
Zeven_div2 [lemma, in Zeven_div2]
Zeven_bool_succ [abbreviation, in Zeven_bool_succ]
Zeven_bool_iff [lemma, in Zeven_bool_iff]
Zeven_mult_Zeven_r [lemma, in Zeven_mult_Zeven_r]
Zeven_ex [lemma, in Zeven_ex]
Zeven_quot2 [lemma, in Zeven_quot2]
Zeven_plus_Zodd [lemma, in Zeven_plus_Zodd]
Zeven_equiv [lemma, in Zeven_equiv]
Zeven_not_Zodd [lemma, in Zeven_not_Zodd]
Zeven_mod [lemma, in Zeven_mod]
Zeven_plus_Zeven [lemma, in Zeven_plus_Zeven]
Zeven_bool_pred [abbreviation, in Zeven_bool_pred]
Zeven_2p [lemma, in Zeven_2p]
Zeven_Sn [lemma, in Zeven_Sn]
Zeven_ex_iff [lemma, in Zeven_ex_iff]
Zeven_rem [lemma, in Zeven_rem]
Zeven_bool [abbreviation, in Zeven_bool]
Zgcd [abbreviation, in Zgcd]
ZGcd [library]
Zgcdn [definition, in Zgcdn]
Zgcdn_opp [lemma, in Zgcdn_opp]
Zgcdn_is_gcd_pos [lemma, in Zgcdn_is_gcd_pos]
Zgcdn_ok_before_fibonacci [lemma, in Zgcdn_ok_before_fibonacci]
Zgcdn_pos [lemma, in Zgcdn_pos]
Zgcdn_is_gcd [lemma, in Zgcdn_is_gcd]
Zgcdn_linear_bound [lemma, in Zgcdn_linear_bound]
Zgcdn_worst_is_fibonacci [lemma, in Zgcdn_worst_is_fibonacci]
ZGcdProp [module, in ZGcdProp]
ZGcdProp.Bezout [definition, in Bezout]
ZGcdProp.Bezout_wd [instance, in Bezout_wd]
ZGcdProp.bezout_1_gcd [lemma, in bezout_1_gcd]
ZGcdProp.divide_1_r [lemma, in divide_1_r]
ZGcdProp.divide_opp_l [lemma, in divide_opp_l]
ZGcdProp.divide_antisym [lemma, in divide_antisym]
ZGcdProp.divide_opp_r [lemma, in divide_opp_r]
ZGcdProp.divide_abs_l [lemma, in divide_abs_l]
ZGcdProp.divide_mul_split [lemma, in divide_mul_split]
ZGcdProp.divide_add_cancel_r [lemma, in divide_add_cancel_r]
ZGcdProp.divide_1_r_abs [lemma, in divide_1_r_abs]
ZGcdProp.divide_sub_r [lemma, in divide_sub_r]
ZGcdProp.divide_antisym_abs [lemma, in divide_antisym_abs]
ZGcdProp.divide_abs_r [lemma, in divide_abs_r]
ZGcdProp.gauss [lemma, in gauss]
ZGcdProp.gcd_abs_l [lemma, in gcd_abs_l]
ZGcdProp.gcd_mul_mono_l [lemma, in gcd_mul_mono_l]
ZGcdProp.gcd_mul_mono_r_nonneg [lemma, in gcd_mul_mono_r_nonneg]
ZGcdProp.gcd_opp_r [lemma, in gcd_opp_r]
ZGcdProp.gcd_add_mult_diag_r [lemma, in gcd_add_mult_diag_r]
ZGcdProp.gcd_0_r [lemma, in gcd_0_r]
ZGcdProp.gcd_mul_mono_r [lemma, in gcd_mul_mono_r]
ZGcdProp.gcd_0_l [lemma, in gcd_0_l]
ZGcdProp.gcd_abs_r [lemma, in gcd_abs_r]
ZGcdProp.gcd_diag [lemma, in gcd_diag]
ZGcdProp.gcd_sub_diag_r [lemma, in gcd_sub_diag_r]
ZGcdProp.gcd_add_diag_r [lemma, in gcd_add_diag_r]
ZGcdProp.gcd_mul_mono_l_nonneg [lemma, in gcd_mul_mono_l_nonneg]
ZGcdProp.gcd_bezout [lemma, in gcd_bezout]
ZGcdProp.gcd_opp_l [lemma, in gcd_opp_l]
Zgcd_nonneg [abbreviation, in Zgcd_nonneg]
Zgcd_spec [lemma, in Zgcd_spec]
Zgcd_is_pos [abbreviation, in Zgcd_is_pos]
Zgcd_comm [abbreviation, in Zgcd_comm]
Zgcd_div_swap [lemma, in Zgcd_div_swap]
Zgcd_greatest [abbreviation, in Zgcd_greatest]
Zgcd_inv_0_r [abbreviation, in Zgcd_inv_0_r]
Zgcd_mult_rel_prime [lemma, in Zgcd_mult_rel_prime]
Zgcd_Zabs [abbreviation, in Zgcd_Zabs]
Zgcd_1_rel_prime [lemma, in Zgcd_1_rel_prime]
Zgcd_0 [abbreviation, in Zgcd_0]
Zgcd_is_gcd [lemma, in Zgcd_is_gcd]
Zgcd_is_gcd [lemma, in Zgcd_is_gcd]
Zgcd_bound_fibonacci [lemma, in Zgcd_bound_fibonacci]
Zgcd_bound_opp [lemma, in Zgcd_bound_opp]
Zgcd_div_swap0 [lemma, in Zgcd_div_swap0]
Zgcd_divide_r [abbreviation, in Zgcd_divide_r]
Zgcd_1 [abbreviation, in Zgcd_1]
Zgcd_bound [lemma, in Zgcd_bound]
Zgcd_bound [definition, in Zgcd_bound]
Zgcd_alt [definition, in Zgcd_alt]
Zgcd_alt_pos [lemma, in Zgcd_alt_pos]
Zgcd_div_pos [lemma, in Zgcd_div_pos]
Zgcd_ass [lemma, in Zgcd_ass]
Zgcd_divide_l [abbreviation, in Zgcd_divide_l]
Zgcd_inv_0_l [abbreviation, in Zgcd_inv_0_l]
Zgcd_alt [library]
Zge [abbreviation, in Zge]
Zge_bool [abbreviation, in Zge_bool]
Zge_cases [lemma, in Zge_cases]
Zge_le [abbreviation, in Zge_le]
Zge_is_le_bool [lemma, in Zge_is_le_bool]
Zge_left [lemma, in Zge_left]
Zge_compare [lemma, in Zge_compare]
Zge_iff_le [abbreviation, in Zge_iff_le]
Zge_trans [lemma, in Zge_trans]
Zge_minus_two_power_nat_S [lemma, in Zge_minus_two_power_nat_S]
Zggcd [abbreviation, in Zggcd]
Zggcd_opp [abbreviation, in Zggcd_opp]
Zggcd_correct_divisors [abbreviation, in Zggcd_correct_divisors]
Zggcd_gcd [abbreviation, in Zggcd_gcd]
Zgt [abbreviation, in Zgt]
Zgt_succ_pred [lemma, in Zgt_succ_pred]
Zgt_not_le [lemma, in Zgt_not_le]
Zgt_left [lemma, in Zgt_left]
Zgt_succ_le [lemma, in Zgt_succ_le]
Zgt_square_simpl [lemma, in Zgt_square_simpl]
Zgt_is_gt_bool [lemma, in Zgt_is_gt_bool]
Zgt_0_le_0_pred [lemma, in Zgt_0_le_0_pred]
Zgt_succ [lemma, in Zgt_succ]
Zgt_trans [lemma, in Zgt_trans]
Zgt_left_rev [lemma, in Zgt_left_rev]
Zgt_cases [lemma, in Zgt_cases]
Zgt_irrefl [lemma, in Zgt_irrefl]
Zgt_bool [abbreviation, in Zgt_bool]
Zgt_le_trans [lemma, in Zgt_le_trans]
Zgt_is_le_bool [lemma, in Zgt_is_le_bool]
Zgt_compare [lemma, in Zgt_compare]
Zgt_iff_lt [abbreviation, in Zgt_iff_lt]
Zgt_le_succ [lemma, in Zgt_le_succ]
Zgt_asym [lemma, in Zgt_asym]
Zgt_pos_0 [lemma, in Zgt_pos_0]
Zgt_lt [abbreviation, in Zgt_lt]
Zgt_succ_gt_or_eq [lemma, in Zgt_succ_gt_or_eq]
Zgt_left_gt [lemma, in Zgt_left_gt]
Zhints [library]
Zind [abbreviation, in Zind]
Zip [section, in Zip]
zipWith [definition, in zipWith]
Zip.A [variable, in A]
Zip.B [variable, in B]
Zip.C [variable, in C]
Zip.f [variable, in f]
Zis_gcd_0 [lemma, in Zis_gcd_0]
Zis_gcd_1 [lemma, in Zis_gcd_1]
Zis_gcd_uniqueness_apart_sign [lemma, in Zis_gcd_uniqueness_apart_sign]
Zis_gcd_mod [lemma, in Zis_gcd_mod]
Zis_gcd_unique [lemma, in Zis_gcd_unique]
Zis_gcd_mult [lemma, in Zis_gcd_mult]
Zis_gcd_minus [lemma, in Zis_gcd_minus]
Zis_gcd_sym [lemma, in Zis_gcd_sym]
Zis_gcd_gcd [lemma, in Zis_gcd_gcd]
Zis_gcd_for_euclid [lemma, in Zis_gcd_for_euclid]
Zis_gcd [inductive, in Zis_gcd]
Zis_gcd_refl [lemma, in Zis_gcd_refl]
Zis_gcd_intro [constructor, in Zis_gcd_intro]
Zis_gcd_rel_prime [lemma, in Zis_gcd_rel_prime]
Zis_gcd_opp [lemma, in Zis_gcd_opp]
Zis_gcd_for_euclid2 [lemma, in Zis_gcd_for_euclid2]
Zis_gcd_0_abs [lemma, in Zis_gcd_0_abs]
Zis_gcd_bezout [lemma, in Zis_gcd_bezout]
ZLcm [library]
ZLcmProp [module, in ZLcmProp]
ZLcmProp.divide_lcm_l [lemma, in divide_lcm_l]
ZLcmProp.divide_lcm_iff [lemma, in divide_lcm_iff]
ZLcmProp.divide_lcm_r [lemma, in divide_lcm_r]
ZLcmProp.divide_quot_mul_exact [lemma, in divide_quot_mul_exact]
ZLcmProp.divide_div [lemma, in divide_div]
ZLcmProp.divide_lcm_eq_r [lemma, in divide_lcm_eq_r]
ZLcmProp.divide_div_mul_exact [lemma, in divide_div_mul_exact]
ZLcmProp.gcd_1_lcm_mul [lemma, in gcd_1_lcm_mul]
ZLcmProp.gcd_quot_factor [lemma, in gcd_quot_factor]
ZLcmProp.gcd_quot_gcd [lemma, in gcd_quot_gcd]
ZLcmProp.gcd_div_factor [lemma, in gcd_div_factor]
ZLcmProp.gcd_rem [lemma, in gcd_rem]
ZLcmProp.gcd_div_gcd [lemma, in gcd_div_gcd]
ZLcmProp.gcd_div_swap [lemma, in gcd_div_swap]
ZLcmProp.gcd_mod [lemma, in gcd_mod]
ZLcmProp.lcm [definition, in lcm]
ZLcmProp.lcm_abs_r [lemma, in lcm_abs_r]
ZLcmProp.lcm_1_l [lemma, in lcm_1_l]
ZLcmProp.lcm_diag_nonneg [lemma, in lcm_diag_nonneg]
ZLcmProp.lcm_0_l [lemma, in lcm_0_l]
ZLcmProp.lcm_0_r [lemma, in lcm_0_r]
ZLcmProp.lcm_least [lemma, in lcm_least]
ZLcmProp.lcm_1_l_nonneg [lemma, in lcm_1_l_nonneg]
ZLcmProp.lcm_wd [instance, in lcm_wd]
ZLcmProp.lcm_equiv1 [lemma, in lcm_equiv1]
ZLcmProp.lcm_1_r [lemma, in lcm_1_r]
ZLcmProp.lcm_mul_mono_l [lemma, in lcm_mul_mono_l]
ZLcmProp.lcm_nonneg [lemma, in lcm_nonneg]
ZLcmProp.lcm_1_r_nonneg [lemma, in lcm_1_r_nonneg]
ZLcmProp.lcm_unique_alt [lemma, in lcm_unique_alt]
ZLcmProp.lcm_abs_l [lemma, in lcm_abs_l]
ZLcmProp.lcm_opp_r [lemma, in lcm_opp_r]
ZLcmProp.lcm_eq_0 [lemma, in lcm_eq_0]
ZLcmProp.lcm_unique [lemma, in lcm_unique]
ZLcmProp.lcm_divide_iff [lemma, in lcm_divide_iff]
ZLcmProp.lcm_assoc [lemma, in lcm_assoc]
ZLcmProp.lcm_equiv2 [lemma, in lcm_equiv2]
ZLcmProp.lcm_mul_mono_r_nonneg [lemma, in lcm_mul_mono_r_nonneg]
ZLcmProp.lcm_mul_mono_l_nonneg [lemma, in lcm_mul_mono_l_nonneg]
ZLcmProp.lcm_comm [lemma, in lcm_comm]
ZLcmProp.lcm_mul_mono_r [lemma, in lcm_mul_mono_r]
ZLcmProp.lcm_opp_l [lemma, in lcm_opp_l]
ZLcmProp.lcm_diag [lemma, in lcm_diag]
ZLcmProp.mod_divide [lemma, in mod_divide]
ZLcmProp.quot_div_nonneg [lemma, in quot_div_nonneg]
ZLcmProp.quot_div_exact [lemma, in quot_div_exact]
ZLcmProp.quot_div [lemma, in quot_div]
ZLcmProp.rem_mod [lemma, in rem_mod]
ZLcmProp.rem_divide [lemma, in rem_divide]
ZLcmProp.rem_mod_eq_0 [lemma, in rem_mod_eq_0]
ZLcmProp.rem_mod_nonneg [lemma, in rem_mod_nonneg]
Zle [abbreviation, in Zle]
Zlength [definition, in Zlength]
Zlength_correct [lemma, in Zlength_correct]
Zlength_nil_inv [lemma, in Zlength_nil_inv]
Zlength_cons [lemma, in Zlength_cons]
Zlength_nil [lemma, in Zlength_nil]
Zlength_aux [definition, in Zlength_aux]
Zlength_properties.A [variable, in A]
Zlength_properties [section, in Zlength_properties]
Zle_bool_imp_le [lemma, in Zle_bool_imp_le]
Zle_pred [abbreviation, in Zle_pred]
Zle_max_r [abbreviation, in Zle_max_r]
Zle_ge [abbreviation, in Zle_ge]
Zle_bool [abbreviation, in Zle_bool]
Zle_bool_trans [lemma, in Zle_bool_trans]
Zle_0_1 [abbreviation, in Zle_0_1]
Zle_bool_total [definition, in Zle_bool_total]
Zle_succ_gt [lemma, in Zle_succ_gt]
Zle_bool_plus_mono [lemma, in Zle_bool_plus_mono]
Zle_neg_pos [lemma, in Zle_neg_pos]
Zle_plus_swap [abbreviation, in Zle_plus_swap]
Zle_left [lemma, in Zle_left]
Zle_0_minus_le [lemma, in Zle_0_minus_le]
Zle_gt_trans [lemma, in Zle_gt_trans]
Zle_min_r [abbreviation, in Zle_min_r]
Zle_cases [lemma, in Zle_cases]
Zle_bool_antisym [lemma, in Zle_bool_antisym]
Zle_is_le_bool [lemma, in Zle_is_le_bool]
Zle_imp_le_bool [lemma, in Zle_imp_le_bool]
Zle_max_l [abbreviation, in Zle_max_l]
Zle_bool_refl [abbreviation, in Zle_bool_refl]
Zle_0_nat [lemma, in Zle_0_nat]
Zle_or_lt [abbreviation, in Zle_or_lt]
Zle_max_compat_r [abbreviation, in Zle_max_compat_r]
Zle_le_succ [abbreviation, in Zle_le_succ]
Zle_max_compat_l [abbreviation, in Zle_max_compat_l]
Zle_minus_le_0 [lemma, in Zle_minus_le_0]
Zle_refl [abbreviation, in Zle_refl]
Zle_0_pos [lemma, in Zle_0_pos]
Zle_antisym [abbreviation, in Zle_antisym]
Zle_trans [abbreviation, in Zle_trans]
Zle_min_compat_l [abbreviation, in Zle_min_compat_l]
Zle_min_l [abbreviation, in Zle_min_l]
Zle_not_gt [lemma, in Zle_not_gt]
Zle_succ [abbreviation, in Zle_succ]
Zle_gt_succ [lemma, in Zle_gt_succ]
Zle_lt_succ [lemma, in Zle_lt_succ]
Zle_succ_le [lemma, in Zle_succ_le]
Zle_compare [lemma, in Zle_compare]
Zle_left_rev [lemma, in Zle_left_rev]
Zle_not_lt [lemma, in Zle_not_lt]
Zle_lt_or_eq_iff [abbreviation, in Zle_lt_or_eq_iff]
Zle_lt_trans [abbreviation, in Zle_lt_trans]
Zle_min_compat_r [abbreviation, in Zle_min_compat_r]
Zle_mult_approx [lemma, in Zle_mult_approx]
Zle_lt_or_eq [lemma, in Zle_lt_or_eq]
Zle_Qle [lemma, in Zle_Qle]
Zle_succ_l [abbreviation, in Zle_succ_l]
Zlogarithm [library]
Zlog2_log_inf [lemma, in Zlog2_log_inf]
Zlog2_up_log_sup [lemma, in Zlog2_up_log_sup]
Zlt [abbreviation, in Zlt]
ZLt [library]
Zlt_succ [abbreviation, in Zlt_succ]
Zlt_compare [lemma, in Zlt_compare]
Zlt_succ_pred [lemma, in Zlt_succ_pred]
Zlt_left_rev [lemma, in Zlt_left_rev]
Zlt_0_le_0_pred [lemma, in Zlt_0_le_0_pred]
Zlt_not_le [lemma, in Zlt_not_le]
Zlt_irrefl [abbreviation, in Zlt_irrefl]
Zlt_plus_swap [abbreviation, in Zlt_plus_swap]
Zlt_0_1 [abbreviation, in Zlt_0_1]
Zlt_gt [abbreviation, in Zlt_gt]
Zlt_trans [abbreviation, in Zlt_trans]
Zlt_two_power_nat_S [lemma, in Zlt_two_power_nat_S]
Zlt_cotrans_pos [lemma, in Zlt_cotrans_pos]
Zlt_left_lt [lemma, in Zlt_left_lt]
Zlt_lower_bound_rec [lemma, in Zlt_lower_bound_rec]
Zlt_cases [lemma, in Zlt_cases]
Zlt_le_succ [lemma, in Zlt_le_succ]
Zlt_le_weak [abbreviation, in Zlt_le_weak]
Zlt_asym [abbreviation, in Zlt_asym]
Zlt_lower_bound_ind [lemma, in Zlt_lower_bound_ind]
Zlt_not_eq [abbreviation, in Zlt_not_eq]
Zlt_succ_r [abbreviation, in Zlt_succ_r]
Zlt_left [lemma, in Zlt_left]
Zlt_is_le_bool [lemma, in Zlt_is_le_bool]
Zlt_minus_simpl_swap [abbreviation, in Zlt_minus_simpl_swap]
Zlt_lt_succ [abbreviation, in Zlt_lt_succ]
Zlt_cotrans_neg [lemma, in Zlt_cotrans_neg]
Zlt_bool [abbreviation, in Zlt_bool]
Zlt_square_simpl [lemma, in Zlt_square_simpl]
Zlt_le_trans [abbreviation, in Zlt_le_trans]
Zlt_0_minus_lt [lemma, in Zlt_0_minus_lt]
Zlt_is_lt_bool [lemma, in Zlt_is_lt_bool]
Zlt_succ_le [lemma, in Zlt_succ_le]
Zlt_pred [abbreviation, in Zlt_pred]
Zlt_Qlt [lemma, in Zlt_Qlt]
Zlt_O_minus_lt [abbreviation, in Zlt_O_minus_lt]
Zlt_cotrans [lemma, in Zlt_cotrans]
Zlt_neg_0 [lemma, in Zlt_neg_0]
Zlt_0_rec [lemma, in Zlt_0_rec]
Zlt_0_ind [lemma, in Zlt_0_ind]
Zlt0_not_eq [lemma, in Zlt0_not_eq]
ZL0 [lemma, in ZL0]
ZL4 [abbreviation, in ZL4]
ZL6 [lemma, in ZL6]
ZMake [library]
Zmax [abbreviation, in Zmax]
Zmax [library]
ZMaxMin [library]
ZMaxMinProp [module, in ZMaxMinProp]
ZMaxMinProp.add_max_distr_r [lemma, in add_max_distr_r]
ZMaxMinProp.add_min_distr_r [lemma, in add_min_distr_r]
ZMaxMinProp.add_min_distr_l [lemma, in add_min_distr_l]
ZMaxMinProp.add_max_distr_l [lemma, in add_max_distr_l]
ZMaxMinProp.mul_max_distr_nonpos_l [lemma, in mul_max_distr_nonpos_l]
ZMaxMinProp.mul_min_distr_nonneg_r [lemma, in mul_min_distr_nonneg_r]
ZMaxMinProp.mul_min_distr_nonpos_r [lemma, in mul_min_distr_nonpos_r]
ZMaxMinProp.mul_min_distr_nonneg_l [lemma, in mul_min_distr_nonneg_l]
ZMaxMinProp.mul_max_distr_nonneg_r [lemma, in mul_max_distr_nonneg_r]
ZMaxMinProp.mul_min_distr_nonpos_l [lemma, in mul_min_distr_nonpos_l]
ZMaxMinProp.mul_max_distr_nonpos_r [lemma, in mul_max_distr_nonpos_r]
ZMaxMinProp.mul_max_distr_nonneg_l [lemma, in mul_max_distr_nonneg_l]
ZMaxMinProp.opp_min_distr [lemma, in opp_min_distr]
ZMaxMinProp.opp_max_distr [lemma, in opp_max_distr]
ZMaxMinProp.pred_max_distr [lemma, in pred_max_distr]
ZMaxMinProp.pred_min_distr [lemma, in pred_min_distr]
ZMaxMinProp.sub_max_distr_r [lemma, in sub_max_distr_r]
ZMaxMinProp.sub_max_distr_l [lemma, in sub_max_distr_l]
ZMaxMinProp.sub_min_distr_l [lemma, in sub_min_distr_l]
ZMaxMinProp.sub_min_distr_r [lemma, in sub_min_distr_r]
ZMaxMinProp.succ_min_distr [lemma, in succ_min_distr]
ZMaxMinProp.succ_max_distr [lemma, in succ_max_distr]
Zmax_min_modular_r [abbreviation, in Zmax_min_modular_r]
Zmax_irreducible_inf [abbreviation, in Zmax_irreducible_inf]
Zmax_comm [abbreviation, in Zmax_comm]
Zmax_case [abbreviation, in Zmax_case]
Zmax_right [abbreviation, in Zmax_right]
Zmax_le_prime_inf [abbreviation, in Zmax_le_prime_inf]
Zmax_n_n [abbreviation, in Zmax_n_n]
Zmax_min_distr_r [abbreviation, in Zmax_min_distr_r]
Zmax_assoc [abbreviation, in Zmax_assoc]
Zmax_le_prime [abbreviation, in Zmax_le_prime]
Zmax_plus [abbreviation, in Zmax_plus]
Zmax_lub [abbreviation, in Zmax_lub]
Zmax_case_strong [abbreviation, in Zmax_case_strong]
Zmax_l [abbreviation, in Zmax_l]
Zmax_lub_lt [abbreviation, in Zmax_lub_lt]
Zmax_idempotent [abbreviation, in Zmax_idempotent]
Zmax_spec [lemma, in Zmax_spec]
Zmax_left [lemma, in Zmax_left]
Zmax_SS [abbreviation, in Zmax_SS]
Zmax_min_absorption_r_r [abbreviation, in Zmax_min_absorption_r_r]
Zmax_irreducible_dec [abbreviation, in Zmax_irreducible_dec]
Zmax_r [abbreviation, in Zmax_r]
Zmax1 [abbreviation, in Zmax1]
Zmax2 [abbreviation, in Zmax2]
Zmin [abbreviation, in Zmin]
Zmin [library]
Zminmax [library]
Zminus [abbreviation, in Zminus]
Zminus_succ_r [abbreviation, in Zminus_succ_r]
Zminus_diag_reverse [lemma, in Zminus_diag_reverse]
Zminus_mod_idemp_r [lemma, in Zminus_mod_idemp_r]
Zminus_eqm [instance, in Zminus_eqm]
Zminus_succ_l [lemma, in Zminus_succ_l]
Zminus_0_l_reverse [lemma, in Zminus_0_l_reverse]
Zminus_mod [lemma, in Zminus_mod]
Zminus_plus [abbreviation, in Zminus_plus]
Zminus_plus_distr [abbreviation, in Zminus_plus_distr]
Zminus_plus_simpl_l [lemma, in Zminus_plus_simpl_l]
Zminus_diag [abbreviation, in Zminus_diag]
Zminus_mod_idemp_l [lemma, in Zminus_mod_idemp_l]
Zminus_plus_simpl_r [lemma, in Zminus_plus_simpl_r]
Zminus_eq [lemma, in Zminus_eq]
Zminus_plus_simpl_l_reverse [lemma, in Zminus_plus_simpl_l_reverse]
Zminus_0_r [abbreviation, in Zminus_0_r]
Zmin_idempotent [abbreviation, in Zmin_idempotent]
Zmin_plus [abbreviation, in Zmin_plus]
Zmin_max_modular_r [abbreviation, in Zmin_max_modular_r]
Zmin_case_strong [abbreviation, in Zmin_case_strong]
Zmin_max_absorption_r_r [abbreviation, in Zmin_max_absorption_r_r]
Zmin_max_distr_r [abbreviation, in Zmin_max_distr_r]
Zmin_le_prime_inf [lemma, in Zmin_le_prime_inf]
Zmin_case [abbreviation, in Zmin_case]
Zmin_comm [abbreviation, in Zmin_comm]
Zmin_glb [abbreviation, in Zmin_glb]
Zmin_r [abbreviation, in Zmin_r]
Zmin_glb_lt [abbreviation, in Zmin_glb_lt]
Zmin_or [abbreviation, in Zmin_or]
Zmin_irreducible_inf [abbreviation, in Zmin_irreducible_inf]
Zmin_SS [abbreviation, in Zmin_SS]
Zmin_irreducible [lemma, in Zmin_irreducible]
Zmin_assoc [abbreviation, in Zmin_assoc]
Zmin_n_n [abbreviation, in Zmin_n_n]
Zmin_l [abbreviation, in Zmin_l]
Zmin_spec [lemma, in Zmin_spec]
Zmisc [library]
Zmod [abbreviation, in Zmod]
ZModulo [section, in ZModulo]
ZModulo [library]
ZModuloCyclicType [module, in ZModuloCyclicType]
ZModuloCyclicType.ops [instance, in ops]
ZModuloCyclicType.specs [instance, in specs]
ZModuloCyclicType.t [definition, in t]
ZModulo.digits [variable, in digits]
ZModulo.digits_gt_1 [variable, in digits_gt_1]
ZModulo.digits_ne_1 [variable, in digits_ne_1]
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
Zmod_div_mod [lemma, in Zmod_div_mod]
Zmod_unique [lemma, in Zmod_unique]
Zmod_divide_minus [lemma, in Zmod_divide_minus]
Zmod_le_first [lemma, in Zmod_le_first]
Zmod_divide [lemma, in Zmod_divide]
Zmod_POS_correct [lemma, in Zmod_POS_correct]
Zmod_eq [lemma, in Zmod_eq]
Zmod_eq_full [lemma, in Zmod_eq_full]
Zmod_1_l [lemma, in Zmod_1_l]
Zmod_opp_opp [lemma, in Zmod_opp_opp]
Zmod_pos_bound [abbreviation, in Zmod_pos_bound]
Zmod_distr [lemma, in Zmod_distr]
Zmod_1_r [lemma, in Zmod_1_r]
Zmod_mod [lemma, in Zmod_mod]
Zmod_POS [definition, in Zmod_POS]
Zmod_POS_bound [abbreviation, in Zmod_POS_bound]
zmod_specs [instance, in zmod_specs]
Zmod_even [lemma, in Zmod_even]
zmod_ops [instance, in zmod_ops]
Zmod_eqm [lemma, in Zmod_eqm]
Zmod_0_l [lemma, in Zmod_0_l]
Zmod_neg_bound [abbreviation, in Zmod_neg_bound]
Zmod_equal [lemma, in Zmod_equal]
Zmod_0_r [lemma, in Zmod_0_r]
Zmod_le [lemma, in Zmod_le]
Zmod_odd [lemma, in Zmod_odd]
Zmod_divides [lemma, in Zmod_divides]
Zmod_small [lemma, in Zmod_small]
Zmod_shift_r [lemma, in Zmod_shift_r]
Zmod_unique_full [lemma, in Zmod_unique_full]
Zmod' [definition, in Zmod']
Zmod'_correct [lemma, in Zmod'_correct]
Zmod2 [definition, in Zmod2]
Zmod2_twice [lemma, in Zmod2_twice]
ZMul [library]
ZMulOrder [library]
ZMulOrderProp [module, in ZMulOrderProp]
ZMulOrderProp.eq_mul_1 [lemma, in eq_mul_1]
ZMulOrderProp.le_mul_diag_r [lemma, in le_mul_diag_r]
ZMulOrderProp.le_0_square [abbreviation, in le_0_square]
ZMulOrderProp.le_0_mul [lemma, in le_0_mul]
ZMulOrderProp.le_mul_0 [lemma, in le_mul_0]
ZMulOrderProp.le_mul_diag_l [lemma, in le_mul_diag_l]
ZMulOrderProp.lt_mul_diag_r [lemma, in lt_mul_diag_r]
ZMulOrderProp.lt_mul_0 [lemma, in lt_mul_0]
ZMulOrderProp.lt_mul_m1_neg [lemma, in lt_mul_m1_neg]
ZMulOrderProp.lt_1_mul_l [lemma, in lt_1_mul_l]
ZMulOrderProp.lt_mul_diag_l [lemma, in lt_mul_diag_l]
ZMulOrderProp.lt_mul_r [lemma, in lt_mul_r]
ZMulOrderProp.lt_m1_mul_r [lemma, in lt_m1_mul_r]
ZMulOrderProp.lt_1_mul_neg [lemma, in lt_1_mul_neg]
ZMulOrderProp.lt_mul_m1_pos [lemma, in lt_mul_m1_pos]
ZMulOrderProp.mul_nonneg [abbreviation, in mul_nonneg]
ZMulOrderProp.mul_pos [abbreviation, in mul_pos]
ZMulOrderProp.mul_nonneg_nonpos [lemma, in mul_nonneg_nonpos]
ZMulOrderProp.mul_nonpos [abbreviation, in mul_nonpos]
ZMulOrderProp.mul_neg [abbreviation, in mul_neg]
ZMulOrderProp.mul_le_mono_nonpos [lemma, in mul_le_mono_nonpos]
ZMulOrderProp.mul_nonpos_nonpos [lemma, in mul_nonpos_nonpos]
ZMulOrderProp.mul_lt_mono_nonpos [lemma, in mul_lt_mono_nonpos]
ZMulOrderProp.mul_nonpos_nonneg [lemma, in mul_nonpos_nonneg]
ZMulOrderProp.mul_eq_1 [definition, in mul_eq_1]
ZMulOrderProp.nlt_square_0 [lemma, in nlt_square_0]
ZMulOrderProp.square_lt_simpl_nonpos [lemma, in square_lt_simpl_nonpos]
ZMulOrderProp.square_le_mono_nonpos [lemma, in square_le_mono_nonpos]
ZMulOrderProp.square_le_simpl_nonpos [lemma, in square_le_simpl_nonpos]
ZMulOrderProp.square_lt_mono_nonpos [lemma, in square_lt_mono_nonpos]
ZMulProp [module, in ZMulProp]
ZMulProp.mul_sub_distr_r [lemma, in mul_sub_distr_r]
ZMulProp.mul_pred_r [lemma, in mul_pred_r]
ZMulProp.mul_sub_distr_l [lemma, in mul_sub_distr_l]
ZMulProp.mul_opp_r [lemma, in mul_opp_r]
ZMulProp.mul_pred_l [lemma, in mul_pred_l]
ZMulProp.mul_opp_comm [lemma, in mul_opp_comm]
ZMulProp.mul_opp_l [lemma, in mul_opp_l]
ZMulProp.mul_opp_opp [lemma, in mul_opp_opp]
Zmult [abbreviation, in Zmult]
Zmult_ge_reg_r [lemma, in Zmult_ge_reg_r]
Zmult_assoc [abbreviation, in Zmult_assoc]
Zmult_succ_l [abbreviation, in Zmult_succ_l]
Zmult_1_r [abbreviation, in Zmult_1_r]
Zmult_gt_0_lt_compat_l [lemma, in Zmult_gt_0_lt_compat_l]
Zmult_lt_0_reg_r_2 [lemma, in Zmult_lt_0_reg_r_2]
Zmult_divide_compat_r [abbreviation, in Zmult_divide_compat_r]
Zmult_eqm [instance, in Zmult_eqm]
Zmult_one [lemma, in Zmult_one]
Zmult_integral [lemma, in Zmult_integral]
Zmult_mod_distr_r [lemma, in Zmult_mod_distr_r]
Zmult_le_0_reg_r [lemma, in Zmult_le_0_reg_r]
Zmult_reg_l [abbreviation, in Zmult_reg_l]
Zmult_divide_compat_l [abbreviation, in Zmult_divide_compat_l]
Zmult_succ_r_reverse [lemma, in Zmult_succ_r_reverse]
Zmult_0_l [abbreviation, in Zmult_0_l]
Zmult_reg_r [abbreviation, in Zmult_reg_r]
Zmult_mod_idemp_r [lemma, in Zmult_mod_idemp_r]
Zmult_gt_reg_r [lemma, in Zmult_gt_reg_r]
Zmult_gt_compat_r [lemma, in Zmult_gt_compat_r]
Zmult_gt_0_le_compat_r [lemma, in Zmult_gt_0_le_compat_r]
Zmult_comm [abbreviation, in Zmult_comm]
Zmult_rem_distr_l [lemma, in Zmult_rem_distr_l]
Zmult_succ_r [abbreviation, in Zmult_succ_r]
Zmult_lt_compat [lemma, in Zmult_lt_compat]
Zmult_ge_compat_l [lemma, in Zmult_ge_compat_l]
Zmult_1_l [abbreviation, in Zmult_1_l]
Zmult_assoc_reverse [lemma, in Zmult_assoc_reverse]
Zmult_gt_compat_l [lemma, in Zmult_gt_compat_l]
Zmult_lt_0_reg_r [lemma, in Zmult_lt_0_reg_r]
Zmult_lt_reg_r [lemma, in Zmult_lt_reg_r]
Zmult_lt_0_le_compat_r [lemma, in Zmult_lt_0_le_compat_r]
Zmult_le_reg_r [lemma, in Zmult_le_reg_r]
Zmult_lt_b [lemma, in Zmult_lt_b]
Zmult_le_compat_r [lemma, in Zmult_le_compat_r]
Zmult_1_inversion_l [abbreviation, in Zmult_1_inversion_l]
Zmult_0_r [abbreviation, in Zmult_0_r]
Zmult_ge_compat_r [lemma, in Zmult_ge_compat_r]
Zmult_lt_0_compat [abbreviation, in Zmult_lt_0_compat]
Zmult_gt_0_lt_reg_r [lemma, in Zmult_gt_0_lt_reg_r]
Zmult_permute [abbreviation, in Zmult_permute]
Zmult_lt_compat_l [lemma, in Zmult_lt_compat_l]
Zmult_le_0_compat [abbreviation, in Zmult_le_0_compat]
Zmult_rem_idemp_l [lemma, in Zmult_rem_idemp_l]
Zmult_mod_distr_l [lemma, in Zmult_mod_distr_l]
Zmult_gt_0_le_0_compat [lemma, in Zmult_gt_0_le_0_compat]
Zmult_lt_O_compat [abbreviation, in Zmult_lt_O_compat]
Zmult_gt_0_compat [lemma, in Zmult_gt_0_compat]
Zmult_plus_distr_r [abbreviation, in Zmult_plus_distr_r]
Zmult_rem_distr_r [lemma, in Zmult_rem_distr_r]
Zmult_le_approx [lemma, in Zmult_le_approx]
Zmult_rem [lemma, in Zmult_rem]
Zmult_0_r_reverse [lemma, in Zmult_0_r_reverse]
Zmult_opp_comm [abbreviation, in Zmult_opp_comm]
Zmult_minus_distr_r [abbreviation, in Zmult_minus_distr_r]
Zmult_gt_0_lt_compat_r [lemma, in Zmult_gt_0_lt_compat_r]
Zmult_power [lemma, in Zmult_power]
Zmult_mod [lemma, in Zmult_mod]
Zmult_lt_compat2 [lemma, in Zmult_lt_compat2]
Zmult_succ_l_reverse [lemma, in Zmult_succ_l_reverse]
Zmult_compare_compat_l [lemma, in Zmult_compare_compat_l]
Zmult_minus_distr_l [lemma, in Zmult_minus_distr_l]
Zmult_integral_l [lemma, in Zmult_integral_l]
Zmult_ge_compat [lemma, in Zmult_ge_compat]
Zmult_opp_opp [abbreviation, in Zmult_opp_opp]
Zmult_le_compat [lemma, in Zmult_le_compat]
Zmult_plus_distr_l [abbreviation, in Zmult_plus_distr_l]
Zmult_lt_0_le_reg_r [lemma, in Zmult_lt_0_le_reg_r]
Zmult_lt_compat_r [lemma, in Zmult_lt_compat_r]
Zmult_compare_compat_r [lemma, in Zmult_compare_compat_r]
Zmult_mod_idemp_l [lemma, in Zmult_mod_idemp_l]
Zmult_gt_0_lt_0_reg_r [lemma, in Zmult_gt_0_lt_0_reg_r]
Zmult_le_compat_l [lemma, in Zmult_le_compat_l]
Zmult_rem_idemp_r [lemma, in Zmult_rem_idemp_r]
Zmult_gt_0_reg_l [lemma, in Zmult_gt_0_reg_l]
Znat [library]
ZNatPairs [library]
Zne [definition, in Zne]
Zneg [constructor, in Zneg]
Zneg [abbreviation, in Zneg]
Zneg_xI [abbreviation, in Zneg_xI]
Zneg_xO [abbreviation, in Zneg_xO]
Zneg_plus_distr [abbreviation, in Zneg_plus_distr]
Zneq_bool [definition, in Zneq_bool]
Zne_left [lemma, in Zne_left]
Znot_le_succ [lemma, in Znot_le_succ]
Znot_ge_lt [lemma, in Znot_ge_lt]
Znot_lt_ge [lemma, in Znot_lt_ge]
Znot_le_gt [lemma, in Znot_le_gt]
Znot_gt_le [lemma, in Znot_gt_le]
Znumtheory [library]
ZnZ [module, in ZnZ]
ZnZ.add [projection, in add]
ZnZ.add_c [projection, in add_c]
ZnZ.add_carry_c [projection, in add_carry_c]
ZnZ.add_carry [projection, in add_carry]
ZnZ.add_mul_div [projection, in add_mul_div]
ZnZ.compare [projection, in compare]
ZnZ.digits [projection, in digits]
ZnZ.div [projection, in div]
ZnZ.div_gt [projection, in div_gt]
ZnZ.div21 [projection, in div21]
ZnZ.eq0 [projection, in eq0]
ZnZ.gcd [projection, in gcd]
ZnZ.gcd_gt [projection, in gcd_gt]
ZnZ.head0 [projection, in head0]
ZnZ.is_even [projection, in is_even]
ZnZ.minus_one [projection, in minus_one]
ZnZ.MkOps [constructor, in MkOps]
ZnZ.MkSpecs [constructor, in MkSpecs]
ZnZ.modulo [projection, in modulo]
ZnZ.modulo_gt [projection, in modulo_gt]
ZnZ.mul [projection, in mul]
ZnZ.mul_c [projection, in mul_c]
ZnZ.of_Z [definition, in of_Z]
ZnZ.of_Z_correct [lemma, in of_Z_correct]
ZnZ.Of_Z [section, in Of_Z]
ZnZ.of_pos [projection, in of_pos]
ZnZ.of_pos_correct [lemma, in of_pos_correct]
[| _ |] [notation, in ::'[|'_x_'|]']
ZnZ.one [projection, in one]
ZnZ.opp [projection, in opp]
ZnZ.opp_carry [projection, in opp_carry]
ZnZ.opp_c [projection, in opp_c]
ZnZ.Ops [record, in Ops]
ZnZ.OW [definition, in OW]
ZnZ.OW' [definition, in OW']
ZnZ.pos_mod [projection, in pos_mod]
ZnZ.pred [projection, in pred]
ZnZ.pred_c [projection, in pred_c]
ZnZ.Specs [record, in Specs]
ZnZ.Specs [section, in Specs]
ZnZ.Specs.wB [variable, in wB]
[+| _ |] [notation, in ::'[+|'_x_'|]']
[-| _ |] [notation, in ::'[-|'_x_'|]']
[| _ |] [notation, in ::'[|'_x_'|]']
[|| _ ||] [notation, in ::'[||'_x_'||]']
ZnZ.spec_pred_c [projection, in spec_pred_c]
ZnZ.spec_add_mul_div [projection, in spec_add_mul_div]
ZnZ.spec_eq0 [projection, in spec_eq0]
ZnZ.spec_of_pos [projection, in spec_of_pos]
ZnZ.spec_sqrt2 [projection, in spec_sqrt2]
ZnZ.spec_div21 [projection, in spec_div21]
ZnZ.spec_is_even [projection, in spec_is_even]
ZnZ.spec_pred [projection, in spec_pred]
ZnZ.spec_head00 [projection, in spec_head00]
ZnZ.spec_OW [lemma, in spec_OW]
ZnZ.spec_add [projection, in spec_add]
ZnZ.spec_WW [lemma, in spec_WW]
ZnZ.spec_zdigits [projection, in spec_zdigits]
ZnZ.spec_succ_c [projection, in spec_succ_c]
ZnZ.spec_mul [projection, in spec_mul]
ZnZ.spec_head0 [projection, in spec_head0]
ZnZ.spec_tail00 [projection, in spec_tail00]
ZnZ.spec_opp_c [projection, in spec_opp_c]
ZnZ.spec_square_c [projection, in spec_square_c]
ZnZ.spec_sub_carry [projection, in spec_sub_carry]
ZnZ.spec_1 [projection, in spec_1]
ZnZ.spec_m1 [projection, in spec_m1]
ZnZ.spec_tail0 [projection, in spec_tail0]
ZnZ.spec_modulo [projection, in spec_modulo]
ZnZ.spec_compare [projection, in spec_compare]
ZnZ.spec_WO [lemma, in spec_WO]
ZnZ.spec_div [projection, in spec_div]
ZnZ.spec_modulo_gt [projection, in spec_modulo_gt]
ZnZ.spec_to_Z [projection, in spec_to_Z]
ZnZ.spec_sub [projection, in spec_sub]
ZnZ.spec_pos_mod [projection, in spec_pos_mod]
ZnZ.spec_succ [projection, in spec_succ]
ZnZ.spec_gcd_gt [projection, in spec_gcd_gt]
ZnZ.spec_opp_carry [projection, in spec_opp_carry]
ZnZ.spec_add_carry_c [projection, in spec_add_carry_c]
ZnZ.spec_sqrt [projection, in spec_sqrt]
ZnZ.spec_add_c [projection, in spec_add_c]
ZnZ.spec_opp [projection, in spec_opp]
ZnZ.spec_sub_c [projection, in spec_sub_c]
ZnZ.spec_add_carry [projection, in spec_add_carry]
ZnZ.spec_gcd [projection, in spec_gcd]
ZnZ.spec_sub_carry_c [projection, in spec_sub_carry_c]
ZnZ.spec_0 [projection, in spec_0]
ZnZ.spec_mul_c [projection, in spec_mul_c]
ZnZ.spec_div_gt [projection, in spec_div_gt]
ZnZ.spec_more_than_1_digit [projection, in spec_more_than_1_digit]
ZnZ.sqrt [projection, in sqrt]
ZnZ.sqrt2 [projection, in sqrt2]
ZnZ.square_c [projection, in square_c]
ZnZ.sub [projection, in sub]
ZnZ.sub_carry_c [projection, in sub_carry_c]
ZnZ.sub_c [projection, in sub_c]
ZnZ.sub_carry [projection, in sub_carry]
ZnZ.succ [projection, in succ]
ZnZ.succ_c [projection, in succ_c]
ZnZ.tail0 [projection, in tail0]
ZnZ.to_Z [projection, in to_Z]
ZnZ.WO [definition, in WO]
ZnZ.WO' [definition, in WO']
ZnZ.WW [definition, in WW]
ZnZ.WW [section, in WW]
ZnZ.WW' [definition, in WW']
ZnZ.WW.wB [variable, in wB]
ZnZ.zdigits [projection, in zdigits]
ZnZ.zero [projection, in zero]
Zn2Z [section, in Zn2Z]
zn2z [inductive, in zn2z]
zn2z_to_Z [definition, in zn2z_to_Z]
zn2z_word_comm [definition, in zn2z_word_comm]
Zn2Z.znz [variable, in znz]
Zodd [definition, in Zodd]
Zodd_bool_iff [lemma, in Zodd_bool_iff]
Zodd_quot2 [lemma, in Zodd_quot2]
Zodd_bool_pred [abbreviation, in Zodd_bool_pred]
Zodd_bool [abbreviation, in Zodd_bool]
Zodd_quot2_neg [lemma, in Zodd_quot2_neg]
Zodd_plus_Zodd [lemma, in Zodd_plus_Zodd]
Zodd_pred [lemma, in Zodd_pred]
Zodd_ex_iff [lemma, in Zodd_ex_iff]
Zodd_bool_succ [abbreviation, in Zodd_bool_succ]
Zodd_Sn [lemma, in Zodd_Sn]
Zodd_mult_Zodd [lemma, in Zodd_mult_Zodd]
Zodd_rem [lemma, in Zodd_rem]
Zodd_equiv [lemma, in Zodd_equiv]
Zodd_plus_Zeven [lemma, in Zodd_plus_Zeven]
Zodd_bit_value [lemma, in Zodd_bit_value]
Zodd_div2 [lemma, in Zodd_div2]
Zodd_2p_plus_1 [lemma, in Zodd_2p_plus_1]
Zodd_mod [lemma, in Zodd_mod]
Zodd_ex [lemma, in Zodd_ex]
Zodd_dec [definition, in Zodd_dec]
Zodd_not_Zeven [lemma, in Zodd_not_Zeven]
Zodd_even_bool [lemma, in Zodd_even_bool]
ZOdiv [abbreviation, in ZOdiv]
ZOdiv [library]
ZOdiv_lt_upper_bound [abbreviation, in ZOdiv_lt_upper_bound]
ZOdiv_le_lower_bound [abbreviation, in ZOdiv_le_lower_bound]
ZOdiv_mult_cancel_l [abbreviation, in ZOdiv_mult_cancel_l]
ZOdiv_eucl_correct [abbreviation, in ZOdiv_eucl_correct]
ZOdiv_opp_opp [abbreviation, in ZOdiv_opp_opp]
ZOdiv_le_upper_bound [abbreviation, in ZOdiv_le_upper_bound]
ZOdiv_small [abbreviation, in ZOdiv_small]
ZOdiv_unique_full [abbreviation, in ZOdiv_unique_full]
ZOdiv_mult_cancel_r [abbreviation, in ZOdiv_mult_cancel_r]
ZOdiv_mult_le [abbreviation, in ZOdiv_mult_le]
ZOdiv_ZOdiv [abbreviation, in ZOdiv_ZOdiv]
ZOdiv_1_l [abbreviation, in ZOdiv_1_l]
ZOdiv_mod_unique_full [abbreviation, in ZOdiv_mod_unique_full]
ZOdiv_eucl_Zdiv_eucl_pos [abbreviation, in ZOdiv_eucl_Zdiv_eucl_pos]
ZOdiv_0_l [abbreviation, in ZOdiv_0_l]
ZOdiv_opp_l [abbreviation, in ZOdiv_opp_l]
ZOdiv_1_r [abbreviation, in ZOdiv_1_r]
ZOdiv_eucl [abbreviation, in ZOdiv_eucl]
ZOdiv_sgn [abbreviation, in ZOdiv_sgn]
ZOdiv_opp_r [abbreviation, in ZOdiv_opp_r]
ZOdiv_unique [abbreviation, in ZOdiv_unique]
ZOdiv_Zdiv_pos [abbreviation, in ZOdiv_Zdiv_pos]
ZOdiv_0_r [abbreviation, in ZOdiv_0_r]
ZOdiv_def [library]
ZOmod [abbreviation, in ZOmod]
ZOmod_lt_neg_pos [abbreviation, in ZOmod_lt_neg_pos]
ZOmod_sgn2 [abbreviation, in ZOmod_sgn2]
ZOmod_sgn [abbreviation, in ZOmod_sgn]
ZOmod_Zmod_pos [abbreviation, in ZOmod_Zmod_pos]
ZOmod_opp_opp [abbreviation, in ZOmod_opp_opp]
ZOmod_0_r [abbreviation, in ZOmod_0_r]
ZOmod_lt_pos [abbreviation, in ZOmod_lt_pos]
ZOmod_opp_r [abbreviation, in ZOmod_opp_r]
ZOmod_divides [abbreviation, in ZOmod_divides]
ZOmod_lt_pos_neg [abbreviation, in ZOmod_lt_pos_neg]
ZOmod_unique_full [abbreviation, in ZOmod_unique_full]
ZOmod_Zmod_zero [abbreviation, in ZOmod_Zmod_zero]
ZOmod_lt_pos_pos [abbreviation, in ZOmod_lt_pos_pos]
ZOmod_1_r [abbreviation, in ZOmod_1_r]
ZOmod_lt_neg_neg [abbreviation, in ZOmod_lt_neg_neg]
ZOmod_small [abbreviation, in ZOmod_small]
ZOmod_opp_l [abbreviation, in ZOmod_opp_l]
ZOmod_mod [abbreviation, in ZOmod_mod]
ZOmod_0_l [abbreviation, in ZOmod_0_l]
ZOmod_le [abbreviation, in ZOmod_le]
ZOmod_lt [abbreviation, in ZOmod_lt]
ZOmod_unique [abbreviation, in ZOmod_unique]
ZOmod_lt_neg [abbreviation, in ZOmod_lt_neg]
ZOmod_1_l [abbreviation, in ZOmod_1_l]
ZOmult_mod_distr_l [abbreviation, in ZOmult_mod_distr_l]
ZOmult_mod_idemp_r [abbreviation, in ZOmult_mod_idemp_r]
ZOmult_mod_idemp_l [abbreviation, in ZOmult_mod_idemp_l]
ZOmult_mod [abbreviation, in ZOmult_mod]
ZOmult_mod_distr_r [abbreviation, in ZOmult_mod_distr_r]
Zone_min_pos [lemma, in Zone_min_pos]
Zone_pos [lemma, in Zone_pos]
Zone_divide [abbreviation, in Zone_divide]
ZOplus_mod_idemp_l [abbreviation, in ZOplus_mod_idemp_l]
ZOplus_mod_idemp_r [abbreviation, in ZOplus_mod_idemp_r]
ZOplus_mod [abbreviation, in ZOplus_mod]
Zopp [abbreviation, in Zopp]
Zopp_involutive [abbreviation, in Zopp_involutive]
Zopp_neg [abbreviation, in Zopp_neg]
Zopp_0 [abbreviation, in Zopp_0]
Zopp_succ [abbreviation, in Zopp_succ]
Zopp_mult_distr_l [lemma, in Zopp_mult_distr_l]
Zopp_mult_distr_l_reverse [abbreviation, in Zopp_mult_distr_l_reverse]
Zopp_mult_distr_r [lemma, in Zopp_mult_distr_r]
Zopp_plus_distr [abbreviation, in Zopp_plus_distr]
Zopp_inj [abbreviation, in Zopp_inj]
Zopp_eqm [instance, in Zopp_eqm]
Zopp_eq_mult_neg_1 [abbreviation, in Zopp_eq_mult_neg_1]
Zorder [library]
ZOrderProp [module, in ZOrderProp]
ZOrderProp.le_le_pred [lemma, in le_le_pred]
ZOrderProp.le_pred_lt_succ [lemma, in le_pred_lt_succ]
ZOrderProp.le_succ_le_pred [lemma, in le_succ_le_pred]
ZOrderProp.le_pred_l [lemma, in le_pred_l]
ZOrderProp.le_pred_lt [lemma, in le_pred_lt]
ZOrderProp.lt_m1_r [lemma, in lt_m1_r]
ZOrderProp.lt_pred_le [lemma, in lt_pred_le]
ZOrderProp.lt_pred_l [lemma, in lt_pred_l]
ZOrderProp.lt_pred_lt [lemma, in lt_pred_lt]
ZOrderProp.lt_le_pred [lemma, in lt_le_pred]
ZOrderProp.lt_succ_lt_pred [lemma, in lt_succ_lt_pred]
ZOrderProp.lt_lt_pred [lemma, in lt_lt_pred]
ZOrderProp.lt_pred_lt_succ [lemma, in lt_pred_lt_succ]
ZOrderProp.neg_nonneg_cases [lemma, in neg_nonneg_cases]
ZOrderProp.neg_pos_cases [lemma, in neg_pos_cases]
ZOrderProp.neq_pred_l [lemma, in neq_pred_l]
ZOrderProp.nle_pred_r [lemma, in nle_pred_r]
ZOrderProp.nonpos_pos_cases [lemma, in nonpos_pos_cases]
ZOrderProp.nonpos_nonneg_cases [lemma, in nonpos_nonneg_cases]
ZOrderProp.pred_lt_mono [lemma, in pred_lt_mono]
ZOrderProp.pred_le_mono [lemma, in pred_le_mono]
ZO_mult_div_ge [abbreviation, in ZO_mult_div_ge]
ZO_mod_mult [abbreviation, in ZO_mod_mult]
ZO_mult_div_le [abbreviation, in ZO_mult_div_le]
ZO_div_plus_l [abbreviation, in ZO_div_plus_l]
ZO_div_monotone [abbreviation, in ZO_div_monotone]
ZO_div_same [abbreviation, in ZO_div_same]
ZO_div_exact_full_2 [definition, in ZO_div_exact_full_2]
ZO_div_lt [abbreviation, in ZO_div_lt]
ZO_mod_same [abbreviation, in ZO_mod_same]
ZO_div_mod_eq [abbreviation, in ZO_div_mod_eq]
ZO_mod_plus [abbreviation, in ZO_mod_plus]
ZO_div_exact_full_1 [definition, in ZO_div_exact_full_1]
ZO_div_pos [abbreviation, in ZO_div_pos]
ZO_div_mult [abbreviation, in ZO_div_mult]
ZO_div_plus [abbreviation, in ZO_div_plus]
ZPairsAxiomsMod [module, in ZPairsAxiomsMod]
ZPairsAxiomsMod.add [definition, in add]
ZPairsAxiomsMod.add_succ_l [lemma, in add_succ_l]
ZPairsAxiomsMod.add_0_l [lemma, in add_0_l]
ZPairsAxiomsMod.add_wd [instance, in add_wd]
ZPairsAxiomsMod.bi_induction [lemma, in bi_induction]
ZPairsAxiomsMod.eq [definition, in eq]
ZPairsAxiomsMod.eq_equiv [instance, in eq_equiv]
ZPairsAxiomsMod.Induction [section, in Induction]
ZPairsAxiomsMod.Induction.A [variable, in A]
ZPairsAxiomsMod.Induction.A_wd [variable, in A_wd]
ZPairsAxiomsMod.le [definition, in le]
ZPairsAxiomsMod.lt [definition, in lt]
ZPairsAxiomsMod.lt_irrefl [lemma, in lt_irrefl]
ZPairsAxiomsMod.lt_eq_cases [lemma, in lt_eq_cases]
ZPairsAxiomsMod.lt_nge [lemma, in lt_nge]
ZPairsAxiomsMod.lt_succ_r [lemma, in lt_succ_r]
ZPairsAxiomsMod.lt_wd [instance, in lt_wd]
ZPairsAxiomsMod.max [definition, in max]
ZPairsAxiomsMod.max_r [lemma, in max_r]
ZPairsAxiomsMod.max_l [lemma, in max_l]
ZPairsAxiomsMod.min [definition, in min]
ZPairsAxiomsMod.min_r [lemma, in min_r]
ZPairsAxiomsMod.min_l [lemma, in min_l]
ZPairsAxiomsMod.mul [definition, in mul]
ZPairsAxiomsMod.mul_succ_l [lemma, in mul_succ_l]
ZPairsAxiomsMod.mul_0_l [lemma, in mul_0_l]
ZPairsAxiomsMod.mul_comm [lemma, in mul_comm]
ZPairsAxiomsMod.mul_wd [instance, in mul_wd]
ZPairsAxiomsMod.NProp [module, in ZPairsAxiomsMod.NProp]
ZPairsAxiomsMod.one [definition, in one]
ZPairsAxiomsMod.one_succ [lemma, in one_succ]
ZPairsAxiomsMod.opp [definition, in opp]
ZPairsAxiomsMod.opp_succ [lemma, in opp_succ]
ZPairsAxiomsMod.opp_wd [instance, in opp_wd]
ZPairsAxiomsMod.opp_0 [lemma, in opp_0]
ZPairsAxiomsMod.pair_wd [instance, in pair_wd]
ZPairsAxiomsMod.pred [definition, in pred]
ZPairsAxiomsMod.pred_succ [lemma, in pred_succ]
ZPairsAxiomsMod.pred_wd [instance, in pred_wd]
ZPairsAxiomsMod.sub [definition, in sub]
ZPairsAxiomsMod.sub_wd [instance, in sub_wd]
ZPairsAxiomsMod.sub_add_opp [lemma, in sub_add_opp]
ZPairsAxiomsMod.sub_succ_r [lemma, in sub_succ_r]
ZPairsAxiomsMod.sub_0_r [lemma, in sub_0_r]
ZPairsAxiomsMod.succ [definition, in succ]
ZPairsAxiomsMod.succ_wd [instance, in succ_wd]
ZPairsAxiomsMod.succ_pred [lemma, in succ_pred]
ZPairsAxiomsMod.t [definition, in t]
ZPairsAxiomsMod.two [definition, in two]
ZPairsAxiomsMod.two_succ [lemma, in two_succ]
ZPairsAxiomsMod.Z [module, in ZPairsAxiomsMod.Z]
ZPairsAxiomsMod.zero [definition, in zero]
ZPairsAxiomsMod.Z.add [definition, in add]
ZPairsAxiomsMod.Z.eq [definition, in eq]
ZPairsAxiomsMod.Z.le [definition, in le]
ZPairsAxiomsMod.Z.lt [definition, in lt]
ZPairsAxiomsMod.Z.max [definition, in max]
ZPairsAxiomsMod.Z.min [definition, in min]
ZPairsAxiomsMod.Z.mul [definition, in mul]
ZPairsAxiomsMod.Z.one [definition, in one]
ZPairsAxiomsMod.Z.opp [definition, in opp]
ZPairsAxiomsMod.Z.pred [definition, in pred]
ZPairsAxiomsMod.Z.sub [definition, in sub]
ZPairsAxiomsMod.Z.succ [definition, in succ]
ZPairsAxiomsMod.Z.t [definition, in t]
ZPairsAxiomsMod.Z.two [definition, in two]
ZPairsAxiomsMod.Z.zero [definition, in zero]
_ <= _ (NScope) [notation, in :NScope:x_'<='_x]
_ + _ (NScope) [notation, in :NScope:x_'+'_x]
_ * _ (NScope) [notation, in :NScope:x_'*'_x]
_ == _ (NScope) [notation, in :NScope:x_'=='_x]
_ ~= _ (NScope) [notation, in :NScope:x_'~='_x]
_ - _ (NScope) [notation, in :NScope:x_'-'_x]
_ < _ (NScope) [notation, in :NScope:x_'<'_x]
0 (NScope) [notation, in :NScope:'0']
1 (NScope) [notation, in :NScope:'1']
2 (NScope) [notation, in :NScope:'2']
_ ~= _ (ZScope) [notation, in :ZScope:x_'~='_x]
_ - _ (ZScope) [notation, in :ZScope:x_'-'_x]
_ * _ (ZScope) [notation, in :ZScope:x_'*'_x]
_ < _ (ZScope) [notation, in :ZScope:x_'<'_x]
_ <= _ (ZScope) [notation, in :ZScope:x_'<='_x]
_ == _ (ZScope) [notation, in :ZScope:x_'=='_x]
_ + _ (ZScope) [notation, in :ZScope:x_'+'_x]
- _ (ZScope) [notation, in :ZScope:'-'_x]
0 (ZScope) [notation, in :ZScope:'0']
1 (ZScope) [notation, in :ZScope:'1']
2 (ZScope) [notation, in :ZScope:'2']
ZParity [library]
ZParityProp [module, in ZParityProp]
ZParityProp.even_sub [lemma, in even_sub]
ZParityProp.even_opp [lemma, in even_opp]
ZParityProp.even_pred [lemma, in even_pred]
ZParityProp.odd_opp [lemma, in odd_opp]
ZParityProp.odd_sub [lemma, in odd_sub]
ZParityProp.odd_pred [lemma, in odd_pred]
Zplus [abbreviation, in Zplus]
Zplus_0_l [abbreviation, in Zplus_0_l]
Zplus_permute [abbreviation, in Zplus_permute]
Zplus_minus_eq [lemma, in Zplus_minus_eq]
Zplus_lt_le_compat [abbreviation, in Zplus_lt_le_compat]
Zplus_comm [abbreviation, in Zplus_comm]
Zplus_mod [lemma, in Zplus_mod]
Zplus_lt_compat_l [lemma, in Zplus_lt_compat_l]
Zplus_opp_r [abbreviation, in Zplus_opp_r]
Zplus_compare_compat [lemma, in Zplus_compare_compat]
Zplus_0_r [abbreviation, in Zplus_0_r]
Zplus_le_0_compat [abbreviation, in Zplus_le_0_compat]
Zplus_rem_idemp_r [lemma, in Zplus_rem_idemp_r]
Zplus_rem_idemp_l [lemma, in Zplus_rem_idemp_l]
Zplus_succ_l [abbreviation, in Zplus_succ_l]
Zplus_lt_compat_r [lemma, in Zplus_lt_compat_r]
Zplus_eq_compat [lemma, in Zplus_eq_compat]
Zplus_0_r_reverse [lemma, in Zplus_0_r_reverse]
Zplus_mod_one [lemma, in Zplus_mod_one]
Zplus_le_compat_r [lemma, in Zplus_le_compat_r]
Zplus_gt_compat_r [lemma, in Zplus_gt_compat_r]
Zplus_assoc_reverse [lemma, in Zplus_assoc_reverse]
Zplus_eqm [instance, in Zplus_eqm]
Zplus_diag_eq_mult_2 [lemma, in Zplus_diag_eq_mult_2]
Zplus_mod_idemp_l [lemma, in Zplus_mod_idemp_l]
Zplus_opp_l [abbreviation, in Zplus_opp_l]
Zplus_lt_reg_l [lemma, in Zplus_lt_reg_l]
Zplus_max_distr_r [abbreviation, in Zplus_max_distr_r]
Zplus_rem [lemma, in Zplus_rem]
Zplus_le_lt_compat [abbreviation, in Zplus_le_lt_compat]
Zplus_gt_reg_l [lemma, in Zplus_gt_reg_l]
Zplus_gt_reg_r [lemma, in Zplus_gt_reg_r]
Zplus_succ_r [abbreviation, in Zplus_succ_r]
Zplus_lt_reg_r [lemma, in Zplus_lt_reg_r]
Zplus_le_compat [abbreviation, in Zplus_le_compat]
Zplus_max_distr_l [abbreviation, in Zplus_max_distr_l]
Zplus_min_distr_r [abbreviation, in Zplus_min_distr_r]
Zplus_le_reg_l [lemma, in Zplus_le_reg_l]
Zplus_gt_compat_l [lemma, in Zplus_gt_compat_l]
Zplus_lt_compat [abbreviation, in Zplus_lt_compat]
Zplus_succ_r_reverse [lemma, in Zplus_succ_r_reverse]
Zplus_le_reg_r [lemma, in Zplus_le_reg_r]
Zplus_mod_idemp_r [lemma, in Zplus_mod_idemp_r]
Zplus_assoc [abbreviation, in Zplus_assoc]
Zplus_reg_l [abbreviation, in Zplus_reg_l]
Zplus_le_compat_l [lemma, in Zplus_le_compat_l]
Zplus_minus [lemma, in Zplus_minus]
Zplus_succ_comm [abbreviation, in Zplus_succ_comm]
Zplus' [abbreviation, in Zplus']
ZPminus [abbreviation, in ZPminus]
Zpos [constructor, in Zpos]
Zpos [abbreviation, in Zpos]
Zpos_xI [abbreviation, in Zpos_xI]
Zpos_minus [abbreviation, in Zpos_minus]
Zpos_P_of_succ_nat [lemma, in Zpos_P_of_succ_nat]
Zpos_min [abbreviation, in Zpos_min]
Zpos_min_1 [lemma, in Zpos_min_1]
Zpos_eq_Z_of_nat_o_nat_of_P [abbreviation, in Zpos_eq_Z_of_nat_o_nat_of_P]
Zpos_xO [abbreviation, in Zpos_xO]
Zpos_eq_rev [abbreviation, in Zpos_eq_rev]
Zpos_max [abbreviation, in Zpos_max]
Zpos_minus_morphism [abbreviation, in Zpos_minus_morphism]
Zpos_max_1 [lemma, in Zpos_max_1]
Zpos_plus_distr [abbreviation, in Zpos_plus_distr]
Zpos_succ_morphism [abbreviation, in Zpos_succ_morphism]
Zpos_eq [lemma, in Zpos_eq]
Zpos_eq_iff [lemma, in Zpos_eq_iff]
Zpos_mult_morphism [abbreviation, in Zpos_mult_morphism]
ZPow [library]
Zpower [abbreviation, in Zpower]
Zpower [library]
Zpower_1_l [abbreviation, in Zpower_1_l]
Zpower_neg_r [abbreviation, in Zpower_neg_r]
Zpower_nat [definition, in Zpower_nat]
Zpower_NR0 [lemma, in Zpower_NR0]
Zpower_0_r [abbreviation, in Zpower_0_r]
Zpower_0_r [abbreviation, in Zpower_0_r]
Zpower_nat_0_r [lemma, in Zpower_nat_0_r]
Zpower_nat_is_exp [lemma, in Zpower_nat_is_exp]
Zpower_le_monotone3 [lemma, in Zpower_le_monotone3]
Zpower_nat_Zpower [abbreviation, in Zpower_nat_Zpower]
Zpower_nat_Zpower [lemma, in Zpower_nat_Zpower]
Zpower_nat_powerRZ [lemma, in Zpower_nat_powerRZ]
Zpower_nat_Z [lemma, in Zpower_nat_Z]
Zpower_alt_neg_r [lemma, in Zpower_alt_neg_r]
Zpower_alt_0_r [lemma, in Zpower_alt_0_r]
Zpower_exp [lemma, in Zpower_exp]
Zpower_le_monotone2 [abbreviation, in Zpower_le_monotone2]
Zpower_theory [lemma, in Zpower_theory]
Zpower_pos [abbreviation, in Zpower_pos]
Zpower_mod [lemma, in Zpower_mod]
Zpower_gt_1 [lemma, in Zpower_gt_1]
Zpower_1_r [abbreviation, in Zpower_1_r]
Zpower_pos_1_r [lemma, in Zpower_pos_1_r]
Zpower_2 [abbreviation, in Zpower_2]
Zpower_equiv [lemma, in Zpower_equiv]
Zpower_pos_nat [lemma, in Zpower_pos_nat]
Zpower_pos_is_exp [lemma, in Zpower_pos_is_exp]
Zpower_le_monotone_inv [lemma, in Zpower_le_monotone_inv]
Zpower_alt_Ppow [lemma, in Zpower_alt_Ppow]
Zpower_le_monotone [lemma, in Zpower_le_monotone]
Zpower_Qpower [lemma, in Zpower_Qpower]
Zpower_Ppow [abbreviation, in Zpower_Ppow]
Zpower_pos_powerRZ [lemma, in Zpower_pos_powerRZ]
Zpower_mult [abbreviation, in Zpower_mult]
Zpower_gt_0 [abbreviation, in Zpower_gt_0]
Zpower_ge_0 [abbreviation, in Zpower_ge_0]
Zpower_pos_0_l [lemma, in Zpower_pos_0_l]
Zpower_alt_succ_r [lemma, in Zpower_alt_succ_r]
Zpower_0_l [abbreviation, in Zpower_0_l]
Zpower_nat_succ_r [lemma, in Zpower_nat_succ_r]
Zpower_succ_r [abbreviation, in Zpower_succ_r]
Zpower_Zsucc [abbreviation, in Zpower_Zsucc]
Zpower_divide [lemma, in Zpower_divide]
Zpower_pos_1_l [lemma, in Zpower_pos_1_l]
Zpower_nat_powerRZ_absolu [lemma, in Zpower_nat_powerRZ_absolu]
Zpower_Zabs [abbreviation, in Zpower_Zabs]
Zpower_alt [definition, in Zpower_alt]
Zpower_pos_pos [lemma, in Zpower_pos_pos]
Zpower_lt_monotone [lemma, in Zpower_lt_monotone]
Zpower2_le_lin [lemma, in Zpower2_le_lin]
Zpower2_Psize [lemma, in Zpower2_Psize]
Zpower2_lt_lin [lemma, in Zpower2_lt_lin]
ZPowProp [module, in ZPowProp]
ZPowProp.abs_pow [lemma, in abs_pow]
ZPowProp.even_pow [lemma, in even_pow]
ZPowProp.odd_pow [lemma, in odd_pow]
ZPowProp.pow_opp_odd [lemma, in pow_opp_odd]
ZPowProp.pow_twice_r [lemma, in pow_twice_r]
ZPowProp.pow_odd_abs_sgn [lemma, in pow_odd_abs_sgn]
ZPowProp.pow_odd_sgn [lemma, in pow_odd_sgn]
ZPowProp.pow_even_nonneg [lemma, in pow_even_nonneg]
ZPowProp.pow_opp_even [lemma, in pow_opp_even]
ZPowProp.pow_even_abs [lemma, in pow_even_abs]
Zpow_mod [definition, in Zpow_mod]
Zpow_mod_pos_correct [lemma, in Zpow_mod_pos_correct]
Zpow_mod_pos [definition, in Zpow_mod_pos]
Zpow_mod_correct [lemma, in Zpow_mod_correct]
Zpow_def [library]
Zpow_facts [library]
Zpow_alt [library]
Zpred [abbreviation, in Zpred]
Zpred_succ [lemma, in Zpred_succ]
Zpred' [abbreviation, in Zpred']
Zpred'_succ' [abbreviation, in Zpred'_succ']
Zpred'_inj [abbreviation, in Zpred'_inj]
ZProp [module, in ZProp]
ZProperties [library]
ZQuot [module, in ZQuot]
Zquot [library]
ZQuotProp [module, in ZQuotProp]
ZQuotProp.add_rem_idemp_l [lemma, in add_rem_idemp_l]
ZQuotProp.add_rem [lemma, in add_rem]
ZQuotProp.add_rem_idemp_r [lemma, in add_rem_idemp_r]
ZQuotProp.mod_mul_r [lemma, in mod_mul_r]
ZQuotProp.mul_rem [lemma, in mul_rem]
ZQuotProp.mul_rem_distr_r [lemma, in mul_rem_distr_r]
ZQuotProp.mul_rem_idemp_l [lemma, in mul_rem_idemp_l]
ZQuotProp.mul_pred_quot_lt [lemma, in mul_pred_quot_lt]
ZQuotProp.mul_succ_quot_gt [lemma, in mul_succ_quot_gt]
ZQuotProp.mul_rem_idemp_r [lemma, in mul_rem_idemp_r]
ZQuotProp.mul_rem_distr_l [lemma, in mul_rem_distr_l]
ZQuotProp.mul_quot_le [lemma, in mul_quot_le]
ZQuotProp.mul_pred_quot_gt [lemma, in mul_pred_quot_gt]
ZQuotProp.mul_quot_ge [lemma, in mul_quot_ge]
ZQuotProp.mul_succ_quot_lt [lemma, in mul_succ_quot_lt]
ZQuotProp.Private_Div.NZQuot [module, in ZQuotProp.Private_Div.NZQuot]
ZQuotProp.Private_Div.Quot2Div.mod_bound_pos [definition, in mod_bound_pos]
ZQuotProp.Private_Div.Quot2Div.modulo [definition, in modulo]
ZQuotProp.Private_Div.Quot2Div [module, in ZQuotProp.Private_Div.Quot2Div]
ZQuotProp.Private_Div.Quot2Div.mod_wd [definition, in mod_wd]
ZQuotProp.Private_Div.Quot2Div.div [definition, in div]
ZQuotProp.Private_Div.Quot2Div.div_wd [definition, in div_wd]
ZQuotProp.Private_Div [module, in ZQuotProp.Private_Div]
ZQuotProp.Private_Div.Quot2Div.div_mod [definition, in div_mod]
ZQuotProp.quot_opp_l [lemma, in quot_opp_l]
ZQuotProp.quot_unique_exact [lemma, in quot_unique_exact]
ZQuotProp.quot_le_upper_bound [lemma, in quot_le_upper_bound]
ZQuotProp.quot_unique [lemma, in quot_unique]
ZQuotProp.quot_lt_upper_bound [lemma, in quot_lt_upper_bound]
ZQuotProp.quot_small_iff [lemma, in quot_small_iff]
ZQuotProp.quot_opp_r [lemma, in quot_opp_r]
ZQuotProp.quot_mul [lemma, in quot_mul]
ZQuotProp.quot_add [lemma, in quot_add]
ZQuotProp.quot_opp_opp [lemma, in quot_opp_opp]
ZQuotProp.quot_small [lemma, in quot_small]
ZQuotProp.quot_le_compat_l [lemma, in quot_le_compat_l]
ZQuotProp.quot_mul_cancel_r [lemma, in quot_mul_cancel_r]
ZQuotProp.quot_0_l [lemma, in quot_0_l]
ZQuotProp.quot_same [lemma, in quot_same]
ZQuotProp.quot_abs_l [lemma, in quot_abs_l]
ZQuotProp.quot_add_l [lemma, in quot_add_l]
ZQuotProp.quot_le_mono [lemma, in quot_le_mono]
ZQuotProp.quot_lt [lemma, in quot_lt]
ZQuotProp.quot_abs [lemma, in quot_abs]
ZQuotProp.quot_mul_cancel_l [lemma, in quot_mul_cancel_l]
ZQuotProp.quot_abs_r [lemma, in quot_abs_r]
ZQuotProp.quot_exact [lemma, in quot_exact]
ZQuotProp.quot_mul_le [lemma, in quot_mul_le]
ZQuotProp.quot_pos [lemma, in quot_pos]
ZQuotProp.quot_str_pos [lemma, in quot_str_pos]
ZQuotProp.quot_le_lower_bound [lemma, in quot_le_lower_bound]
ZQuotProp.quot_rem_unique [lemma, in quot_rem_unique]
ZQuotProp.quot_1_r [lemma, in quot_1_r]
ZQuotProp.quot_quot [lemma, in quot_quot]
ZQuotProp.quot_1_l [lemma, in quot_1_l]
ZQuotProp.rem_sign_nz [lemma, in rem_sign_nz]
ZQuotProp.rem_sign [lemma, in rem_sign]
ZQuotProp.rem_same [lemma, in rem_same]
ZQuotProp.rem_1_l [lemma, in rem_1_l]
ZQuotProp.rem_abs [lemma, in rem_abs]
ZQuotProp.rem_small_iff [lemma, in rem_small_iff]
ZQuotProp.rem_eq [lemma, in rem_eq]
ZQuotProp.rem_bound_abs [lemma, in rem_bound_abs]
ZQuotProp.rem_mul [lemma, in rem_mul]
ZQuotProp.rem_opp_opp [lemma, in rem_opp_opp]
ZQuotProp.rem_0_l [lemma, in rem_0_l]
ZQuotProp.rem_rem [lemma, in rem_rem]
ZQuotProp.rem_le [lemma, in rem_le]
ZQuotProp.rem_abs_l [lemma, in rem_abs_l]
ZQuotProp.rem_abs_r [lemma, in rem_abs_r]
ZQuotProp.rem_unique [lemma, in rem_unique]
ZQuotProp.rem_add [lemma, in rem_add]
ZQuotProp.rem_1_r [lemma, in rem_1_r]
ZQuotProp.rem_small [lemma, in rem_small]
ZQuotProp.rem_nonpos [lemma, in rem_nonpos]
ZQuotProp.rem_sign_mul [lemma, in rem_sign_mul]
ZQuotProp.rem_nonneg [lemma, in rem_nonneg]
Zquotrem_Zdiv_eucl_pos [lemma, in Zquotrem_Zdiv_eucl_pos]
Zquot_Zdiv_pos [lemma, in Zquot_Zdiv_pos]
Zquot_mult_le [lemma, in Zquot_mult_le]
Zquot_sgn [lemma, in Zquot_sgn]
Zquot_unique [abbreviation, in Zquot_unique]
Zquot_0_r [lemma, in Zquot_0_r]
Zquot_mod_unique_full [lemma, in Zquot_mod_unique_full]
Zquot_mult_cancel_l [lemma, in Zquot_mult_cancel_l]
Zquot_1_l [abbreviation, in Zquot_1_l]
Zquot_lt_upper_bound [lemma, in Zquot_lt_upper_bound]
Zquot_le_lower_bound [lemma, in Zquot_le_lower_bound]
Zquot_Zquot [lemma, in Zquot_Zquot]
Zquot_le_upper_bound [lemma, in Zquot_le_upper_bound]
Zquot_mult_cancel_r [lemma, in Zquot_mult_cancel_r]
Zquot_0_l [lemma, in Zquot_0_l]
Zquot_unique_full [lemma, in Zquot_unique_full]
Zquot_opp_opp [lemma, in Zquot_opp_opp]
Zquot_opp_r [lemma, in Zquot_opp_r]
Zquot_1_r [abbreviation, in Zquot_1_r]
Zquot_small [abbreviation, in Zquot_small]
Zquot_opp_l [lemma, in Zquot_opp_l]
ZQuot' [module, in ZQuot']
Zquot2 [abbreviation, in Zquot2]
Zquot2_opp [lemma, in Zquot2_opp]
Zquot2_odd_remainder [lemma, in Zquot2_odd_remainder]
Zquot2_quot [abbreviation, in Zquot2_quot]
Zquot2_quot [lemma, in Zquot2_quot]
Zquot2_odd_eqn [lemma, in Zquot2_odd_eqn]
Zrel_prime_neq_mod_0 [lemma, in Zrel_prime_neq_mod_0]
Zrem_Zmod_pos [lemma, in Zrem_Zmod_pos]
Zrem_lt_neg_neg [lemma, in Zrem_lt_neg_neg]
Zrem_sgn [lemma, in Zrem_sgn]
Zrem_sgn2 [lemma, in Zrem_sgn2]
Zrem_le [lemma, in Zrem_le]
Zrem_1_r [abbreviation, in Zrem_1_r]
Zrem_unique_full [lemma, in Zrem_unique_full]
Zrem_lt_pos_pos [lemma, in Zrem_lt_pos_pos]
Zrem_lt_neg [lemma, in Zrem_lt_neg]
Zrem_small [abbreviation, in Zrem_small]
Zrem_Zmod_zero [lemma, in Zrem_Zmod_zero]
Zrem_0_l [lemma, in Zrem_0_l]
Zrem_1_l [abbreviation, in Zrem_1_l]
Zrem_lt [abbreviation, in Zrem_lt]
Zrem_opp_opp [lemma, in Zrem_opp_opp]
Zrem_lt_neg_pos [lemma, in Zrem_lt_neg_pos]
Zrem_unique [abbreviation, in Zrem_unique]
Zrem_even [lemma, in Zrem_even]
Zrem_lt_pos_neg [lemma, in Zrem_lt_pos_neg]
Zrem_odd [lemma, in Zrem_odd]
Zrem_lt_pos [lemma, in Zrem_lt_pos]
Zrem_0_r [lemma, in Zrem_0_r]
Zrem_rem [lemma, in Zrem_rem]
Zrem_opp_r [lemma, in Zrem_opp_r]
Zrem_opp_l [lemma, in Zrem_opp_l]
Zrem_divides [lemma, in Zrem_divides]
Zsgn [abbreviation, in Zsgn]
ZSgnAbs [library]
ZSgnAbsProp [module, in ZSgnAbsProp]
ZSgnAbsProp.abs_involutive [lemma, in abs_involutive]
ZSgnAbsProp.abs_eq_iff [lemma, in abs_eq_iff]
ZSgnAbsProp.abs_max [lemma, in abs_max]
ZSgnAbsProp.abs_neq_iff [lemma, in abs_neq_iff]
ZSgnAbsProp.abs_square [lemma, in abs_square]
ZSgnAbsProp.abs_case_strong [lemma, in abs_case_strong]
ZSgnAbsProp.abs_sgn [lemma, in abs_sgn]
ZSgnAbsProp.abs_nonneg [lemma, in abs_nonneg]
ZSgnAbsProp.abs_eq_or_opp [lemma, in abs_eq_or_opp]
ZSgnAbsProp.abs_wd [instance, in abs_wd]
ZSgnAbsProp.abs_lt [lemma, in abs_lt]
ZSgnAbsProp.abs_neq' [lemma, in abs_neq']
ZSgnAbsProp.abs_0_iff [lemma, in abs_0_iff]
ZSgnAbsProp.abs_spec [lemma, in abs_spec]
ZSgnAbsProp.abs_triangle [lemma, in abs_triangle]
ZSgnAbsProp.abs_eq_cases [lemma, in abs_eq_cases]
ZSgnAbsProp.abs_le [lemma, in abs_le]
ZSgnAbsProp.abs_case [lemma, in abs_case]
ZSgnAbsProp.abs_pos [lemma, in abs_pos]
ZSgnAbsProp.abs_mul [lemma, in abs_mul]
ZSgnAbsProp.abs_opp [lemma, in abs_opp]
ZSgnAbsProp.abs_sub_triangle [lemma, in abs_sub_triangle]
ZSgnAbsProp.abs_0 [lemma, in abs_0]
ZSgnAbsProp.abs_or_opp_abs [lemma, in abs_or_opp_abs]
ZSgnAbsProp.sgn_null_iff [lemma, in sgn_null_iff]
ZSgnAbsProp.sgn_nonpos [lemma, in sgn_nonpos]
ZSgnAbsProp.sgn_nonneg [lemma, in sgn_nonneg]
ZSgnAbsProp.sgn_opp [lemma, in sgn_opp]
ZSgnAbsProp.sgn_abs [lemma, in sgn_abs]
ZSgnAbsProp.sgn_sgn [lemma, in sgn_sgn]
ZSgnAbsProp.sgn_wd [instance, in sgn_wd]
ZSgnAbsProp.sgn_pos_iff [lemma, in sgn_pos_iff]
ZSgnAbsProp.sgn_mul [lemma, in sgn_mul]
ZSgnAbsProp.sgn_neg_iff [lemma, in sgn_neg_iff]
ZSgnAbsProp.sgn_spec [lemma, in sgn_spec]
ZSgnAbsProp.sgn_0 [lemma, in sgn_0]
Zsgn_m1 [abbreviation, in Zsgn_m1]
Zsgn_Zabs [abbreviation, in Zsgn_Zabs]
Zsgn_spec [lemma, in Zsgn_spec]
Zsgn_Zmult [abbreviation, in Zsgn_Zmult]
Zsgn_Zopp [abbreviation, in Zsgn_Zopp]
Zsgn_neg [abbreviation, in Zsgn_neg]
Zsgn_pos [abbreviation, in Zsgn_pos]
Zsgn_0 [abbreviation, in Zsgn_0]
Zsgn_null [abbreviation, in Zsgn_null]
Zsgn_1 [abbreviation, in Zsgn_1]
ZSig [library]
ZSigZAxioms [library]
Zsplit2 [lemma, in Zsplit2]
Zsqrt [definition, in Zsqrt]
Zsqrt_interval [lemma, in Zsqrt_interval]
Zsqrt_square_id [lemma, in Zsqrt_square_id]
Zsqrt_equiv [lemma, in Zsqrt_equiv]
Zsqrt_plain [definition, in Zsqrt_plain]
Zsqrt_le [lemma, in Zsqrt_le]
Zsqrt_plain_is_pos [lemma, in Zsqrt_plain_is_pos]
Zsqrt_compat [library]
Zsquare [abbreviation, in Zsquare]
Zsquare_mult [lemma, in Zsquare_mult]
Zsquare_le [lemma, in Zsquare_le]
Zsquare_correct [abbreviation, in Zsquare_correct]
Zsquare_pos [lemma, in Zsquare_pos]
Zsucc [abbreviation, in Zsucc]
Zsucc_lt_compat [lemma, in Zsucc_lt_compat]
Zsucc_le_reg [lemma, in Zsucc_le_reg]
Zsucc_lt_reg [lemma, in Zsucc_lt_reg]
Zsucc_gt_reg [lemma, in Zsucc_gt_reg]
Zsucc_eq_compat [lemma, in Zsucc_eq_compat]
Zsucc_max_distr [abbreviation, in Zsucc_max_distr]
Zsucc_le_compat [lemma, in Zsucc_le_compat]
Zsucc_pred [lemma, in Zsucc_pred]
Zsucc_inj [abbreviation, in Zsucc_inj]
Zsucc_discr [abbreviation, in Zsucc_discr]
Zsucc_gt_compat [lemma, in Zsucc_gt_compat]
Zsucc_min_distr [abbreviation, in Zsucc_min_distr]
Zsucc' [abbreviation, in Zsucc']
Zsucc'_pred' [abbreviation, in Zsucc'_pred']
Zsucc'_inj [abbreviation, in Zsucc'_inj]
Zsucc'_discr [abbreviation, in Zsucc'_discr]
Ztrichotomy [lemma, in Ztrichotomy]
Ztrichotomy_inf [lemma, in Ztrichotomy_inf]
ZType [module, in ZType]
ZTypeIsZAxioms [module, in ZTypeIsZAxioms]
ZTypeIsZAxioms.abs_eq [lemma, in abs_eq]
ZTypeIsZAxioms.abs_neq [lemma, in abs_neq]
ZTypeIsZAxioms.add_succ_l [lemma, in add_succ_l]
ZTypeIsZAxioms.add_0_l [lemma, in add_0_l]
ZTypeIsZAxioms.add_wd [instance, in add_wd]
ZTypeIsZAxioms.bi_induction [lemma, in bi_induction]
ZTypeIsZAxioms.BP [lemma, in BP]
ZTypeIsZAxioms.BS [lemma, in BS]
ZTypeIsZAxioms.B_holds [lemma, in B_holds]
ZTypeIsZAxioms.B0 [lemma, in B0]
ZTypeIsZAxioms.compare_lt_iff [lemma, in compare_lt_iff]
ZTypeIsZAxioms.compare_antisym [lemma, in compare_antisym]
ZTypeIsZAxioms.compare_le_iff [lemma, in compare_le_iff]
ZTypeIsZAxioms.compare_eq_iff [lemma, in compare_eq_iff]
ZTypeIsZAxioms.compare_wd [instance, in compare_wd]
ZTypeIsZAxioms.divide [definition, in divide]
ZTypeIsZAxioms.div_wd [instance, in div_wd]
ZTypeIsZAxioms.div_mod [lemma, in div_mod]
ZTypeIsZAxioms.div2_spec [lemma, in div2_spec]
ZTypeIsZAxioms.eqb_eq [lemma, in eqb_eq]
ZTypeIsZAxioms.eqb_wd [instance, in eqb_wd]
ZTypeIsZAxioms.eq_equiv [instance, in eq_equiv]
ZTypeIsZAxioms.Even [definition, in Even]
ZTypeIsZAxioms.even_spec [lemma, in even_spec]
ZTypeIsZAxioms.gcd_nonneg [lemma, in gcd_nonneg]
ZTypeIsZAxioms.gcd_greatest [lemma, in gcd_greatest]
ZTypeIsZAxioms.gcd_divide_r [lemma, in gcd_divide_r]
ZTypeIsZAxioms.gcd_divide_l [lemma, in gcd_divide_l]
ZTypeIsZAxioms.Induction [section, in Induction]
ZTypeIsZAxioms.Induction.A [variable, in A]
ZTypeIsZAxioms.Induction.AS [variable, in AS]
ZTypeIsZAxioms.Induction.A_wd [variable, in A_wd]
ZTypeIsZAxioms.Induction.A0 [variable, in A0]
ZTypeIsZAxioms.Induction.B [variable, in B]
ZTypeIsZAxioms.land_spec [lemma, in land_spec]
ZTypeIsZAxioms.ldiff_spec [lemma, in ldiff_spec]
ZTypeIsZAxioms.leb_le [lemma, in leb_le]
ZTypeIsZAxioms.leb_wd [instance, in leb_wd]
ZTypeIsZAxioms.log2_spec [lemma, in log2_spec]
ZTypeIsZAxioms.log2_nonpos [lemma, in log2_nonpos]
ZTypeIsZAxioms.lor_spec [lemma, in lor_spec]
ZTypeIsZAxioms.ltb_wd [instance, in ltb_wd]
ZTypeIsZAxioms.ltb_lt [lemma, in ltb_lt]
ZTypeIsZAxioms.lt_succ_r [lemma, in lt_succ_r]
ZTypeIsZAxioms.lt_wd [instance, in lt_wd]
ZTypeIsZAxioms.lxor_spec [lemma, in lxor_spec]
ZTypeIsZAxioms.max_r [lemma, in max_r]
ZTypeIsZAxioms.max_l [lemma, in max_l]
ZTypeIsZAxioms.min_r [lemma, in min_r]
ZTypeIsZAxioms.min_l [lemma, in min_l]
ZTypeIsZAxioms.mod_neg_bound [lemma, in mod_neg_bound]
ZTypeIsZAxioms.mod_bound_pos [definition, in mod_bound_pos]
ZTypeIsZAxioms.mod_wd [instance, in mod_wd]
ZTypeIsZAxioms.mod_pos_bound [lemma, in mod_pos_bound]
ZTypeIsZAxioms.mul_succ_l [lemma, in mul_succ_l]
ZTypeIsZAxioms.mul_0_l [lemma, in mul_0_l]
ZTypeIsZAxioms.mul_wd [instance, in mul_wd]
ZTypeIsZAxioms.Odd [definition, in Odd]
ZTypeIsZAxioms.odd_spec [lemma, in odd_spec]
ZTypeIsZAxioms.one_succ [lemma, in one_succ]
ZTypeIsZAxioms.opp_succ [lemma, in opp_succ]
ZTypeIsZAxioms.opp_wd [instance, in opp_wd]
ZTypeIsZAxioms.opp_0 [lemma, in opp_0]
ZTypeIsZAxioms.pow_wd [instance, in pow_wd]
ZTypeIsZAxioms.pow_pow_N [lemma, in pow_pow_N]
ZTypeIsZAxioms.pow_0_r [lemma, in pow_0_r]
ZTypeIsZAxioms.pow_pos_N [lemma, in pow_pos_N]
ZTypeIsZAxioms.pow_succ_r [lemma, in pow_succ_r]
ZTypeIsZAxioms.pow_neg_r [lemma, in pow_neg_r]
ZTypeIsZAxioms.pred_succ [lemma, in pred_succ]
ZTypeIsZAxioms.pred_wd [instance, in pred_wd]
ZTypeIsZAxioms.quot_rem [lemma, in quot_rem]
ZTypeIsZAxioms.quot_wd [instance, in quot_wd]
ZTypeIsZAxioms.rem_opp_l [lemma, in rem_opp_l]
ZTypeIsZAxioms.rem_bound_pos [lemma, in rem_bound_pos]
ZTypeIsZAxioms.rem_wd [instance, in rem_wd]
ZTypeIsZAxioms.rem_opp_r [lemma, in rem_opp_r]
ZTypeIsZAxioms.sgn_pos [lemma, in sgn_pos]
ZTypeIsZAxioms.sgn_null [lemma, in sgn_null]
ZTypeIsZAxioms.sgn_neg [lemma, in sgn_neg]
ZTypeIsZAxioms.shiftl_spec_low [lemma, in shiftl_spec_low]
ZTypeIsZAxioms.shiftl_spec_high [lemma, in shiftl_spec_high]
ZTypeIsZAxioms.shiftr_spec [lemma, in shiftr_spec]
ZTypeIsZAxioms.spec_divide [lemma, in spec_divide]
ZTypeIsZAxioms.sqrt_spec [lemma, in sqrt_spec]
ZTypeIsZAxioms.sqrt_neg [lemma, in sqrt_neg]
ZTypeIsZAxioms.square_spec [lemma, in square_spec]
ZTypeIsZAxioms.sub_wd [instance, in sub_wd]
ZTypeIsZAxioms.sub_succ_r [lemma, in sub_succ_r]
ZTypeIsZAxioms.sub_0_r [lemma, in sub_0_r]
ZTypeIsZAxioms.succ_wd [instance, in succ_wd]
ZTypeIsZAxioms.succ_pred [lemma, in succ_pred]
ZTypeIsZAxioms.testbit_even_0 [lemma, in testbit_even_0]
ZTypeIsZAxioms.testbit_neg_r [lemma, in testbit_neg_r]
ZTypeIsZAxioms.testbit_even_succ [lemma, in testbit_even_succ]
ZTypeIsZAxioms.testbit_odd_0 [lemma, in testbit_odd_0]
ZTypeIsZAxioms.testbit_odd_succ [lemma, in testbit_odd_succ]
ZTypeIsZAxioms.testbit_wd [instance, in testbit_wd]
ZTypeIsZAxioms.two_succ [lemma, in two_succ]
( _ | _ ) [notation, in ::'('_x_'|'_x_')']
_ ^ _ [notation, in ::x_'^'_x]
_ < _ [notation, in ::x_'<'_x]
ZType_Notation [module, in ZType_Notation]
_ == _ [notation, in ::x_'=='_x]
- _ [notation, in ::'-'_x]
2 [notation, in ::'2']
[ _ ] [notation, in ::'['_x_']']
_ - _ [notation, in ::x_'-'_x]
ZType_ZAxioms [module, in ZType_ZAxioms]
1 [notation, in ::'1']
_ * _ [notation, in ::x_'*'_x]
_ <= _ [notation, in ::x_'<='_x]
_ + _ [notation, in ::x_'+'_x]
0 [notation, in ::'0']
ZType' [module, in ZType']
ZType.abs [axiom, in abs]
ZType.add [axiom, in add]
ZType.compare [axiom, in compare]
ZType.div [axiom, in div]
ZType.div_eucl [axiom, in div_eucl]
ZType.div2 [axiom, in div2]
ZType.eq [definition, in eq]
ZType.eqb [axiom, in eqb]
ZType.even [axiom, in even]
ZType.gcd [axiom, in gcd]
ZType.land [axiom, in land]
ZType.ldiff [axiom, in ldiff]
ZType.le [definition, in le]
ZType.leb [axiom, in leb]
ZType.log2 [axiom, in log2]
ZType.lor [axiom, in lor]
ZType.lt [definition, in lt]
ZType.ltb [axiom, in ltb]
ZType.lxor [axiom, in lxor]
ZType.max [axiom, in max]
ZType.min [axiom, in min]
ZType.minus_one [axiom, in minus_one]
ZType.modulo [axiom, in modulo]
ZType.mul [axiom, in mul]
ZType.odd [axiom, in odd]
ZType.of_Z [axiom, in of_Z]
ZType.one [axiom, in one]
ZType.opp [axiom, in opp]
ZType.pow [axiom, in pow]
ZType.pow_N [axiom, in pow_N]
ZType.pow_pos [axiom, in pow_pos]
ZType.pred [axiom, in pred]
ZType.quot [axiom, in quot]
ZType.rem [axiom, in rem]
ZType.sgn [axiom, in sgn]
ZType.shiftl [axiom, in shiftl]
ZType.shiftr [axiom, in shiftr]
ZType.spec_of_Z [axiom, in spec_of_Z]
ZType.spec_ltb [axiom, in spec_ltb]
ZType.spec_shiftl [axiom, in spec_shiftl]
ZType.spec_pred [axiom, in spec_pred]
ZType.spec_max [axiom, in spec_max]
ZType.spec_sgn [axiom, in spec_sgn]
ZType.spec_leb [axiom, in spec_leb]
ZType.spec_add [axiom, in spec_add]
ZType.spec_land [axiom, in spec_land]
ZType.spec_odd [axiom, in spec_odd]
ZType.spec_shiftr [axiom, in spec_shiftr]
ZType.spec_2 [axiom, in spec_2]
ZType.spec_div2 [axiom, in spec_div2]
ZType.spec_mul [axiom, in spec_mul]
ZType.spec_testbit [axiom, in spec_testbit]
ZType.spec_rem [axiom, in spec_rem]
ZType.spec_1 [axiom, in spec_1]
ZType.spec_quot [axiom, in spec_quot]
ZType.spec_m1 [axiom, in spec_m1]
ZType.spec_eqb [axiom, in spec_eqb]
ZType.spec_lxor [axiom, in spec_lxor]
ZType.spec_modulo [axiom, in spec_modulo]
ZType.spec_compare [axiom, in spec_compare]
ZType.spec_pow [axiom, in spec_pow]
ZType.spec_even [axiom, in spec_even]
ZType.spec_ldiff [axiom, in spec_ldiff]
ZType.spec_div [axiom, in spec_div]
ZType.spec_div_eucl [axiom, in spec_div_eucl]
ZType.spec_pow_pos [axiom, in spec_pow_pos]
ZType.spec_lor [axiom, in spec_lor]
ZType.spec_sub [axiom, in spec_sub]
ZType.spec_succ [axiom, in spec_succ]
ZType.spec_abs [axiom, in spec_abs]
ZType.spec_sqrt [axiom, in spec_sqrt]
ZType.spec_min [axiom, in spec_min]
ZType.spec_opp [axiom, in spec_opp]
ZType.spec_log2 [axiom, in spec_log2]
ZType.spec_gcd [axiom, in spec_gcd]
ZType.spec_pow_N [axiom, in spec_pow_N]
ZType.spec_square [axiom, in spec_square]
ZType.spec_0 [axiom, in spec_0]
ZType.sqrt [axiom, in sqrt]
ZType.square [axiom, in square]
ZType.sub [axiom, in sub]
ZType.succ [axiom, in succ]
ZType.t [axiom, in t]
ZType.testbit [axiom, in testbit]
ZType.to_Z [axiom, in to_Z]
ZType.two [axiom, in two]
ZType.zero [axiom, in zero]
[ _ ] [notation, in ::'['_x_']']
Zwf [definition, in Zwf]
Zwf [library]
Zwf_up_well_founded [lemma, in Zwf_up_well_founded]
Zwf_up [definition, in Zwf_up]
Zwf_well_founded [lemma, in Zwf_well_founded]
Z_div_mod_eq [lemma, in Z_div_mod_eq]
Z_2nZ.w_opp [variable, in w_opp]
Z_2nZ.w_mod_gt [variable, in w_mod_gt]
Z_2nZ.spec_ww_sqrt2 [variable, in spec_ww_sqrt2]
Z_R_minus [lemma, in Z_R_minus]
Z_of_N_gt_iff [abbreviation, in Z_of_N_gt_iff]
Z_quot_lt [lemma, in Z_quot_lt]
Z_gt_le_dec [definition, in Z_gt_le_dec]
Z_gt_le_bool [definition, in Z_gt_le_bool]
Z_2nZ.mul [variable, in mul]
Z_lt_abs_induction [lemma, in Z_lt_abs_induction]
Z_2nZ.gcd [variable, in gcd]
Z_div_lt [lemma, in Z_div_lt]
Z_zerop [lemma, in Z_zerop]
Z_ge_lt_dec [definition, in Z_ge_lt_dec]
Z_2nZ.spec_ww_opp [variable, in spec_ww_opp]
Z_2nZ.sub [variable, in sub]
Z_as_Int.i2z_2 [lemma, in i2z_2]
Z_notzerop [lemma, in Z_notzerop]
Z_of_nat_complete [lemma, in Z_of_nat_complete]
Z_as_OT.eq_refl [definition, in eq_refl]
Z_2nZ.spec_ww_head0 [variable, in spec_ww_head0]
Z_2nZ.spec_ww_digits [variable, in spec_ww_digits]
Z_2nZ.sub_carry_c [variable, in sub_carry_c]
Z_2nZ.succ [variable, in succ]
Z_2nZ.wB [variable, in wB]
Z_2nZ.spec_low [variable, in spec_low]
Z_mod_lt [lemma, in Z_mod_lt]
Z_of_N_plus [abbreviation, in Z_of_N_plus]
Z_eq_dec [abbreviation, in Z_eq_dec]
Z_div2_value [lemma, in Z_div2_value]
Z_2nZ.w_is_even [variable, in w_is_even]
Z_div_plus_full [lemma, in Z_div_plus_full]
Z_2nZ.gcd_gt [variable, in gcd_gt]
Z_of_N_gt_rev [abbreviation, in Z_of_N_gt_rev]
Z_2nZ.w_sub_carry_c [variable, in w_sub_carry_c]
Z_2nZ.spec_ww_gcd [variable, in spec_ww_gcd]
Z_of_nat_of_N [abbreviation, in Z_of_nat_of_N]
Z_2nZ.w_of_pos [variable, in w_of_pos]
Z_mod_nz_opp_r [lemma, in Z_mod_nz_opp_r]
Z_2nZ.w_div21 [variable, in w_div21]
Z_mod_mult [lemma, in Z_mod_mult]
Z_2nZ.add [variable, in add]
Z_rem_same [lemma, in Z_rem_same]
Z_dec [lemma, in Z_dec]
Z_as_Int.int [definition, in int]
Z_2nZ.w_gcd [variable, in w_gcd]
Z_div_zero_opp_r [lemma, in Z_div_zero_opp_r]
Z_as_Int.i2z_mult [lemma, in i2z_mult]
Z_rect [abbreviation, in Z_rect]
Z_ge_lt_bool [definition, in Z_ge_lt_bool]
Z_div_nz_opp_r [lemma, in Z_div_nz_opp_r]
[[ _ ]] [notation, in ::'[['_x_']]']
Z_div_plus [lemma, in Z_div_plus]
Z_as_Int.i2z_max [lemma, in i2z_max]
Z_2nZ.square_c [variable, in square_c]
Z_div_same_full [lemma, in Z_div_same_full]
Z_2nZ.gcd_gt_fix [variable, in gcd_gt_fix]
Z_le_lt_eq_dec [definition, in Z_le_lt_eq_dec]
Z_div_exact_2 [lemma, in Z_div_exact_2]
Z_2nZ.spec_add2 [variable, in spec_add2]
Z_2nZ.w_gcd_gt [variable, in w_gcd_gt]
Z_2nZ.spec_ww_eq0 [variable, in spec_ww_eq0]
Z_2nZ.w_add2 [variable, in w_add2]
Z_2nZ.spec_ww_sub [variable, in spec_ww_sub]
Z_div_plus_l [definition, in Z_div_plus_l]
Z_as_Int [module, in Z_as_Int]
Z_eq_bool [definition, in Z_eq_bool]
Z_of_N_eq [abbreviation, in Z_of_N_eq]
Z_2nZ.w_eq0 [variable, in w_eq0]
Z_gt_dec [definition, in Z_gt_dec]
Z_2nZ.w_digits [variable, in w_digits]
Z_2nZ.spec_ww_add_c [variable, in spec_ww_add_c]
Z_div_exact_full_2 [lemma, in Z_div_exact_full_2]
Z_0_1_more [lemma, in Z_0_1_more]
Z_2nZ.spec_ww_1 [variable, in spec_ww_1]
Z_of_N_le_rev [abbreviation, in Z_of_N_le_rev]
Z_of_N [abbreviation, in Z_of_N]
Z_div_mod_POS [lemma, in Z_div_mod_POS]
Z_of_N_le_iff [abbreviation, in Z_of_N_le_iff]
Z_of_N_pos [abbreviation, in Z_of_N_pos]
Z_2nZ.w_pos_mod [variable, in w_pos_mod]
Z_as_Int.i2z_eq [lemma, in i2z_eq]
Z_2nZ.gcd_cont [variable, in gcd_cont]
Z_to_binary [lemma, in Z_to_binary]
Z_2nZ.w_mul_c [variable, in w_mul_c]
Z_of_N_ge [abbreviation, in Z_of_N_ge]
Z_2nZ.spec_ww_mul_c [variable, in spec_ww_mul_c]
Z_2nZ.tail0 [variable, in tail0]
Z_mult_div_ge_neg [lemma, in Z_mult_div_ge_neg]
Z_2nZ._ww_digits [variable, in _ww_digits]
Z_as_Int.max [definition, in max]
Z_nat_N [lemma, in Z_nat_N]
Z_2nZ.eq0 [variable, in eq0]
Z_div_pos [lemma, in Z_div_pos]
Z_2nZ.is_even [variable, in is_even]
Z_mod_zero_opp_full [lemma, in Z_mod_zero_opp_full]
Z_2nZ.spec_ww_Bm1 [variable, in spec_ww_Bm1]
Z_2nZ.w_add_carry_c [variable, in w_add_carry_c]
Z_lt_ge_dec [definition, in Z_lt_ge_dec]
Z_as_Int.ge_lt_dec [definition, in ge_lt_dec]
Z_2nZ.sub_c [variable, in sub_c]
Z_mod_plus [lemma, in Z_mod_plus]
Z_quot_mult [abbreviation, in Z_quot_mult]
Z_2nZ.div_gt [variable, in div_gt]
Z_2nZ.mod_gt [variable, in mod_gt]
Z_quot_same [abbreviation, in Z_quot_same]
Z_lt_ge_bool [definition, in Z_lt_ge_bool]
Z_N_nat [lemma, in Z_N_nat]
Z_2nZ.w_head0 [variable, in w_head0]
Z_2nZ._zn2z [variable, in _zn2z]
Z_2nZ.spec_ww_pred [variable, in spec_ww_pred]
Z_2nZ.opp_carry [variable, in opp_carry]
Z_mod_remainder [lemma, in Z_mod_remainder]
Z_div_mod [lemma, in Z_div_mod]
Z_2nZ.sub_carry [variable, in sub_carry]
Z_as_Int.minus [definition, in minus]
Z_as_OT.t [definition, in t]
Z_as_Int.t [definition, in t]
Z_div_plus_full_l [lemma, in Z_div_plus_full_l]
Z_to_binary_to_Z [lemma, in Z_to_binary_to_Z]
Z_2nZ.to_Z [variable, in to_Z]
Z_to_two_compl_to_Z [lemma, in Z_to_two_compl_to_Z]
Z_mod_zero_opp [lemma, in Z_mod_zero_opp]
Z_as_Int._2 [definition, in _2]
Z_2nZ.wwB [variable, in wwB]
Z_2nZ.add_c [variable, in add_c]
Z_2nZ.spec_ww_square_c [variable, in spec_ww_square_c]
Z_2nZ.w_sub [variable, in w_sub]
Z_as_Int._0 [definition, in _0]
Z_2nZ.spec_ww_sub_carry [variable, in spec_ww_sub_carry]
Z_2nZ.w_compare [variable, in w_compare]
Z_noteq_bool [definition, in Z_noteq_bool]
Z_as_OT.compare [definition, in compare]
Z_2nZ.compare [variable, in compare]
Z_2nZ.w_succ [variable, in w_succ]
Z_of_N_le_0 [abbreviation, in Z_of_N_le_0]
Z_2nZ.spec_ww_opp_c [variable, in spec_ww_opp_c]
Z_mod_nz_opp_full [lemma, in Z_mod_nz_opp_full]
Z_2nZ.spec_ww_0 [variable, in spec_ww_0]
Z_2nZ.head0 [variable, in head0]
Z_2nZ.spec_ww_is_even [variable, in spec_ww_is_even]
Z_2nZ.w_sub_c [variable, in w_sub_c]
Z_2nZ.w_opp_c [variable, in w_opp_c]
Z_lt_induction [lemma, in Z_lt_induction]
Z_2nZ.pred_c [variable, in pred_c]
Z_as_Int.i2z_1 [lemma, in i2z_1]
Z_of_nat_of_P [abbreviation, in Z_of_nat_of_P]
Z_BRIC_A_BRAC [section, in Z_BRIC_A_BRAC]
Z_2nZ.spec_ww_sqrt [variable, in spec_ww_sqrt]
Z_mod_neg [lemma, in Z_mod_neg]
Z_2nZ.mod_ [variable, in mod_]
Z_2nZ.karatsuba_c [variable, in karatsuba_c]
Z_lt_dec [definition, in Z_lt_dec]
Z_2nZ.w_div [variable, in w_div]
Z_2nZ.sqrt2 [variable, in sqrt2]
Z_2nZ.add_carry_c [variable, in add_carry_c]
Z_of_N_ge_rev [abbreviation, in Z_of_N_ge_rev]
Z_mult_div_ge [lemma, in Z_mult_div_ge]
Z_2nZ.spec_ww_div [variable, in spec_ww_div]
Z_2nZ.w_add_c [variable, in w_add_c]
Z_div_le [lemma, in Z_div_le]
Z_mod_same_full [lemma, in Z_mod_same_full]
Z_of_nat_prop [lemma, in Z_of_nat_prop]
Z_div_mult [lemma, in Z_div_mult]
Z_2nZ.spec_ww_tail00 [variable, in spec_ww_tail00]
Z_2nZ.spec_ww_of_pos [variable, in spec_ww_of_pos]
Z_2nZ.mul_c [variable, in mul_c]
Z_2nZ.w_add [variable, in w_add]
Z_as_Int._1 [definition, in _1]
Z_2nZ.w_1 [variable, in w_1]
Z_2nZ.ww_of_pos [variable, in ww_of_pos]
Z_le_gt_dec [definition, in Z_le_gt_dec]
Z_of_N_min [abbreviation, in Z_of_N_min]
Z_2nZ.w_div_gt [variable, in w_div_gt]
Z_of_N_eq_rev [abbreviation, in Z_of_N_eq_rev]
Z_of_nat_set [lemma, in Z_of_nat_set]
Z_of_N_lt_rev [abbreviation, in Z_of_N_lt_rev]
Z_as_Int.i2z_plus [lemma, in i2z_plus]
Z_2nZ.w_mul [variable, in w_mul]
Z_2nZ [section, in Z_2nZ]
Z_as_Int.plus [definition, in plus]
Z_rem_mult [lemma, in Z_rem_mult]
Z_2nZ.spec_ww_div_gt [variable, in spec_ww_div_gt]
Z_2nZ.w_succ_c [variable, in w_succ_c]
Z_2nZ.spec_ww_add [variable, in spec_ww_add]
Z_as_Int.i2z_0 [lemma, in i2z_0]
Z_2nZ.spec_ww_sub_carry_c [variable, in spec_ww_sub_carry_c]
Z_div_same [lemma, in Z_div_same]
Z_ge_dec [definition, in Z_ge_dec]
Z_of_N_lt_iff [abbreviation, in Z_of_N_lt_iff]
Z_of_N_abs [abbreviation, in Z_of_N_abs]
Z_ind [abbreviation, in Z_ind]
Z_of_nat_complete_inf [lemma, in Z_of_nat_complete_inf]
Z_div_exact_full_1 [lemma, in Z_div_exact_full_1]
Z_div_nz_opp_full [lemma, in Z_div_nz_opp_full]
Z_2nZ.w_to_Z [variable, in w_to_Z]
Z_div_ge [lemma, in Z_div_ge]
Z_as_Int.i2z [definition, in i2z]
Z_noteq_dec [lemma, in Z_noteq_dec]
Z_2nZ.pred [variable, in pred]
Z_quot_plus_l [lemma, in Z_quot_plus_l]
Z_2nZ.w_Bm1 [variable, in w_Bm1]
Z_of_N_ge_iff [abbreviation, in Z_of_N_ge_iff]
Z_2nZ.spec_ww_compare [variable, in spec_ww_compare]
Z_as_OT.eq_sym [definition, in eq_sym]
Z_le_dec [definition, in Z_le_dec]
Z_2nZ.ww_0W [variable, in ww_0W]
Z_2nZ.w_sub_carry [variable, in w_sub_carry]
Z_div_mult_full [lemma, in Z_div_mult_full]
Z_of_N_eq_iff [abbreviation, in Z_of_N_eq_iff]
Z_mod_plus_full [lemma, in Z_mod_plus_full]
Z_quot_pos [lemma, in Z_quot_pos]
Z_2nZ.spec_ww_gcd_gt [variable, in spec_ww_gcd_gt]
Z_quot_plus [lemma, in Z_quot_plus]
Z_of_nat [abbreviation, in Z_of_nat]
Z_2nZ.spec_ww_sub_c [variable, in spec_ww_sub_c]
Z_2nZ.spec_ww_add_carry [variable, in spec_ww_add_carry]
Z_as_OT.lt_not_eq [lemma, in lt_not_eq]
Z_2nZ.add_carry [variable, in add_carry]
Z_lt_abs_rec [lemma, in Z_lt_abs_rec]
Z_2nZ.w_add_carry [variable, in w_add_carry]
Z_2nZ.sqrt [variable, in sqrt]
Z_2nZ.ww_W0 [variable, in ww_W0]
Z_as_Int.i2z_minus [lemma, in i2z_minus]
Z_2nZ.opp [variable, in opp]
Z_as_Int.opp [definition, in opp]
Z_div_zero_opp_full [lemma, in Z_div_zero_opp_full]
[| _ |] [notation, in ::'[|'_x_'|]']
Z_of_N_lt [abbreviation, in Z_of_N_lt]
Z_2nZ.ww_Bm1 [variable, in ww_Bm1]
Z_to_two_compl_Sn [lemma, in Z_to_two_compl_Sn]
Z_2nZ.spec_ww_mul [variable, in spec_ww_mul]
Z_2nZ.w_opp_carry [variable, in w_opp_carry]
Z_as_OT.lt_trans [lemma, in lt_trans]
Z_as_Int.i2z_3 [lemma, in i2z_3]
Z_2nZ.div [variable, in div]
Z_of_N_mult [abbreviation, in Z_of_N_mult]
Z_quot_rem_eq [abbreviation, in Z_quot_rem_eq]
Z_lt_le_dec [lemma, in Z_lt_le_dec]
Z_2nZ.w_WW [variable, in w_WW]
Z_2nZ.spec_ww_karatsuba_c [variable, in spec_ww_karatsuba_c]
Z_as_OT.eq_trans [definition, in eq_trans]
Z_of_N_le [abbreviation, in Z_of_N_le]
Z_rem_plus [lemma, in Z_rem_plus]
Z_as_Int.mult [definition, in mult]
Z_2nZ.add_mul_div [variable, in add_mul_div]
Z_quot_monotone [lemma, in Z_quot_monotone]
Z_to_binary_Sn_z [lemma, in Z_to_binary_Sn_z]
Z_of_N_minus [abbreviation, in Z_of_N_minus]
Z_as_Int.gt_le_dec [definition, in gt_le_dec]
Z_2nZ.spec_ww_mod [variable, in spec_ww_mod]
Z_div_exact_1 [lemma, in Z_div_exact_1]
Z_as_OT.eq_dec [definition, in eq_dec]
Z_as_Int.eq_dec [definition, in eq_dec]
Z_2nZ.w_add_mul_div [variable, in w_add_mul_div]
Z_2nZ.w_pred_c [variable, in w_pred_c]
Z_2nZ.w_pred [variable, in w_pred]
Z_to_two_compl_Sn_z [lemma, in Z_to_two_compl_Sn_z]
Z_eq_mult [lemma, in Z_eq_mult]
Z_2nZ.div32 [variable, in div32]
Z_as_Int._3 [definition, in _3]
Z_quot_exact_full [lemma, in Z_quot_exact_full]
Z_lt_rec [lemma, in Z_lt_rec]
Z_2nZ._ww_zdigits [variable, in _ww_zdigits]
[-| _ |] [notation, in ::'[-|'_x_'|]']
Z_to_two_compl [lemma, in Z_to_two_compl]
Z_dec' [lemma, in Z_dec']
Z_2nZ.spec_ww_head00 [variable, in spec_ww_head00]
Z_2nZ.w_0 [variable, in w_0]
Z_div_ge0 [lemma, in Z_div_ge0]
Z_as_Int.i2z_opp [lemma, in i2z_opp]
Z_rec [abbreviation, in Z_rec]
Z_as_OT [module, in Z_as_OT]
Z_as_OT [module, in Z_as_OT]
Z_of_N_succ [abbreviation, in Z_of_N_succ]
Z_2nZ.ww_1 [variable, in ww_1]
Z_of_N_compare [abbreviation, in Z_of_N_compare]
Z_2nZ.w_sqrt2 [variable, in w_sqrt2]
Z_mod_same [lemma, in Z_mod_same]
Z_of_N_of_nat [abbreviation, in Z_of_N_of_nat]
Z_mult_quot_le [lemma, in Z_mult_quot_le]
Z_2nZ.w_W0 [variable, in w_W0]
Z_modulo_2 [lemma, in Z_modulo_2]
Z_2nZ.w_sqrt [variable, in w_sqrt]
Z_to_binary_Sn [lemma, in Z_to_binary_Sn]
Z_2nZ.pos_mod [variable, in pos_mod]
Z_div_mod_eq_full [abbreviation, in Z_div_mod_eq_full]
Z_2nZ.ww_WW [variable, in ww_WW]
Z_mod_zero_opp_r [lemma, in Z_mod_zero_opp_r]
Z_2nZ.spec_ww_tail0 [variable, in spec_ww_tail0]
Z_as_OT.lt [definition, in lt]
[+| _ |] [notation, in ::'[+|'_x_'|]']
Z_2nZ.w_square_c [variable, in w_square_c]
Z_2nZ.opp_c [variable, in opp_c]
Z_2nZ.spec_ww_pred_c [variable, in spec_ww_pred_c]
Z_div_mod_full [lemma, in Z_div_mod_full]
Z_le_gt_bool [definition, in Z_le_gt_bool]
Z_2nZ.succ_c [variable, in succ_c]
Z_2nZ.low [variable, in low]
Z_2nZ.w_mod [variable, in w_mod]
Z_2nZ.spec_ww_div21 [variable, in spec_ww_div21]
Z_2nZ.spec_ww_opp_carry [variable, in spec_ww_opp_carry]
Z_of_N_gt [abbreviation, in Z_of_N_gt]
Z_2nZ.div21 [variable, in div21]
Z_mult_quot_ge [lemma, in Z_mult_quot_ge]
Z_2nZ.spec_ww_add_carry_c [variable, in spec_ww_add_carry_c]
Z_as_DT [module, in Z_as_DT]
Z_as_DT [module, in Z_as_DT]
Z_2nZ.w_Bm2 [variable, in w_Bm2]
Z_2nZ.spec_ww_succ [variable, in spec_ww_succ]
Z_2nZ.spec_ww_mod_gt [variable, in spec_ww_mod_gt]
Z_as_OT.eq [definition, in eq]
Z_2nZ.w_0W [variable, in w_0W]
Z_2nZ.spec_w_div32 [variable, in spec_w_div32]
Z_2nZ.w_zdigits [variable, in w_zdigits]
Z_2nZ.spec_ww_to_Z [variable, in spec_ww_to_Z]
Z_2nZ.w_tail0 [variable, in w_tail0]
Z_of_N_max [abbreviation, in Z_of_N_max]
Z_2nZ.spec_ww_succ_c [variable, in spec_ww_succ_c]
Z.abs [definition, in abs]
Z.abs_N [definition, in abs_N]
Z.abs_eq [lemma, in abs_eq]
Z.abs_nat [definition, in abs_nat]
Z.abs_neq [lemma, in abs_neq]
Z.add [definition, in add]
Z.add_diag [lemma, in add_diag]
Z.add_succ_l [lemma, in add_succ_l]
Z.add_reg_l [lemma, in add_reg_l]
Z.add_compare_mono_l [lemma, in add_compare_mono_l]
Z.add_0_l [lemma, in add_0_l]
Z.add_wd [definition, in add_wd]
Z.bi_induction [lemma, in bi_induction]
Z.compare [definition, in compare]
Z.compare_lt_iff [lemma, in compare_lt_iff]
Z.compare_antisym [lemma, in compare_antisym]
Z.compare_le_iff [lemma, in compare_le_iff]
Z.compare_eq_iff [lemma, in compare_eq_iff]
Z.compare_sub [lemma, in compare_sub]
Z.compare_opp [lemma, in compare_opp]
Z.div [definition, in div]
Z.divide [definition, in divide]
Z.div_eucl [definition, in div_eucl]
Z.div_eucl_eq [lemma, in div_eucl_eq]
Z.div_wd [definition, in div_wd]
Z.div_mod [lemma, in div_mod]
Z.div2 [definition, in div2]
Z.div2_spec [lemma, in div2_spec]
Z.double [definition, in double]
Z.double_spec [lemma, in double_spec]
Z.eq [definition, in eq]
Z.eqb [definition, in eqb]
Z.eqb_eq [lemma, in eqb_eq]
Z.eq_dec [definition, in eq_dec]
Z.eq_equiv [definition, in eq_equiv]
Z.Even [definition, in Even]
Z.even [definition, in even]
Z.even_spec [lemma, in even_spec]
Z.gcd [definition, in gcd]
Z.gcd_nonneg [lemma, in gcd_nonneg]
Z.gcd_greatest [lemma, in gcd_greatest]
Z.gcd_divide_r [lemma, in gcd_divide_r]
Z.gcd_divide_l [lemma, in gcd_divide_l]
Z.ge [definition, in ge]
Z.geb [definition, in geb]
Z.geb_spec [lemma, in geb_spec]
Z.geb_leb [lemma, in geb_leb]
Z.geb_le [lemma, in geb_le]
Z.ge_le [lemma, in ge_le]
Z.ge_le_iff [lemma, in ge_le_iff]
Z.ggcd [definition, in ggcd]
Z.ggcd_correct_divisors [lemma, in ggcd_correct_divisors]
Z.ggcd_opp [lemma, in ggcd_opp]
Z.ggcd_gcd [lemma, in ggcd_gcd]
Z.gt [definition, in gt]
Z.gtb [definition, in gtb]
Z.gtb_spec [lemma, in gtb_spec]
Z.gtb_lt [lemma, in gtb_lt]
Z.gtb_ltb [lemma, in gtb_ltb]
Z.gt_lt [lemma, in gt_lt]
Z.gt_lt_iff [lemma, in gt_lt_iff]
Z.iter [definition, in iter]
Z.land [definition, in land]
Z.land_spec [lemma, in land_spec]
Z.ldiff [definition, in ldiff]
Z.ldiff_spec [lemma, in ldiff_spec]
Z.le [definition, in le]
Z.leb [definition, in leb]
Z.leb_le [lemma, in leb_le]
Z.le_ge [lemma, in le_ge]
Z.log2 [definition, in log2]
Z.log2_spec [lemma, in log2_spec]
Z.log2_nonpos [lemma, in log2_nonpos]
Z.lor [definition, in lor]
Z.lor_spec [lemma, in lor_spec]
Z.lt [definition, in lt]
Z.ltb [definition, in ltb]
Z.ltb_lt [lemma, in ltb_lt]
Z.lt_succ_r [lemma, in lt_succ_r]
Z.lt_gt [lemma, in lt_gt]
Z.lt_wd [definition, in lt_wd]
Z.lxor [definition, in lxor]
Z.lxor_spec [lemma, in lxor_spec]
Z.max [definition, in max]
Z.max_r [lemma, in max_r]
Z.max_l [lemma, in max_l]
Z.min [definition, in min]
Z.min_r [lemma, in min_r]
Z.min_l [lemma, in min_l]
Z.modulo [definition, in modulo]
Z.mod_neg_bound [lemma, in mod_neg_bound]
Z.mod_bound_pos [definition, in mod_bound_pos]
Z.mod_wd [definition, in mod_wd]
Z.mod_pos_bound [lemma, in mod_pos_bound]
Z.mul [definition, in mul]
Z.mul_reg_l [lemma, in mul_reg_l]
Z.mul_succ_l [lemma, in mul_succ_l]
Z.mul_reg_r [lemma, in mul_reg_r]
Z.mul_0_l [lemma, in mul_0_l]
Z.mul_wd [definition, in mul_wd]
Z.neg [abbreviation, in neg]
Z.odd [definition, in odd]
Z.Odd [definition, in Odd]
Z.odd_spec [lemma, in odd_spec]
Z.of_nat [definition, in of_nat]
Z.of_N [definition, in of_N]
Z.one [definition, in one]
Z.one_succ [lemma, in one_succ]
Z.opp [definition, in opp]
Z.opp_eq_mul_m1 [lemma, in opp_eq_mul_m1]
Z.opp_succ [lemma, in opp_succ]
Z.opp_wd [definition, in opp_wd]
Z.opp_0 [lemma, in opp_0]
Z.peano_ind [lemma, in peano_ind]
Z.pos [abbreviation, in pos]
Z.pos_sub_gt [lemma, in pos_sub_gt]
Z.pos_div_eucl [definition, in pos_div_eucl]
Z.pos_div_eucl_bound [lemma, in pos_div_eucl_bound]
Z.pos_sub_spec [lemma, in pos_sub_spec]
Z.pos_sub_opp [lemma, in pos_sub_opp]
Z.pos_sub_lt [lemma, in pos_sub_lt]
Z.pos_div_eucl_eq [lemma, in pos_div_eucl_eq]
Z.pos_sub_diag [lemma, in pos_sub_diag]
Z.pos_sub_discr [lemma, in pos_sub_discr]
Z.pos_sub [definition, in pos_sub]
Z.pow [definition, in pow]
Z.pow_wd [definition, in pow_wd]
Z.pow_0_r [lemma, in pow_0_r]
Z.pow_pos_fold [lemma, in pow_pos_fold]
Z.pow_succ_r [lemma, in pow_succ_r]
Z.pow_pos [definition, in pow_pos]
Z.pow_neg_r [lemma, in pow_neg_r]
Z.pred [definition, in pred]
Z.pred_double [definition, in pred_double]
Z.pred_double_spec [lemma, in pred_double_spec]
Z.pred_succ [lemma, in pred_succ]
Z.pred_wd [definition, in pred_wd]
Z.Private_BootStrap.add_opp_diag_l [lemma, in add_opp_diag_l]
Z.Private_BootStrap.divide_Zpos_Zneg_l [lemma, in divide_Zpos_Zneg_l]
Z.Private_BootStrap.mul_1_r [lemma, in mul_1_r]
Z.Private_BootStrap.add_opp_diag_r [lemma, in add_opp_diag_r]
Z.Private_BootStrap.mul_add_distr_l [lemma, in mul_add_distr_l]
Z.Private_BootStrap.mul_add_distr_pos [lemma, in mul_add_distr_pos]
Z.Private_BootStrap.add_0_r [lemma, in add_0_r]
Z.Private_BootStrap.testbit_of_N [lemma, in testbit_of_N]
Z.Private_BootStrap.sub_succ_l [lemma, in sub_succ_l]
Z.Private_BootStrap.divide_Zpos_Zneg_r [lemma, in divide_Zpos_Zneg_r]
Z.Private_BootStrap.mul_opp_r [lemma, in mul_opp_r]
Z.Private_BootStrap.add_assoc [lemma, in add_assoc]
Z.Private_BootStrap.add_comm [lemma, in add_comm]
Z.Private_BootStrap.testbit_Zneg [lemma, in testbit_Zneg]
Z.Private_BootStrap.testbit_of_N' [lemma, in testbit_of_N']
Z.Private_BootStrap.mul_1_l [lemma, in mul_1_l]
Z.Private_BootStrap [module, in Z.Private_BootStrap]
Z.Private_BootStrap.mul_add_distr_r [lemma, in mul_add_distr_r]
Z.Private_BootStrap.pos_sub_add [lemma, in pos_sub_add]
Z.Private_BootStrap.mul_comm [lemma, in mul_comm]
Z.Private_BootStrap.mul_opp_comm [lemma, in mul_opp_comm]
Z.Private_BootStrap.mul_opp_l [lemma, in mul_opp_l]
Z.Private_BootStrap.mul_assoc [lemma, in mul_assoc]
Z.Private_BootStrap.mul_opp_opp [lemma, in mul_opp_opp]
Z.Private_BootStrap.opp_inj [lemma, in opp_inj]
Z.Private_BootStrap.divide_Zpos [lemma, in divide_Zpos]
Z.Private_BootStrap.testbit_Zpos [lemma, in testbit_Zpos]
Z.Private_BootStrap.opp_add_distr [lemma, in opp_add_distr]
Z.quot [definition, in quot]
Z.quotrem [definition, in quotrem]
Z.quotrem_eq [lemma, in quotrem_eq]
Z.quot_rem [lemma, in quot_rem]
Z.quot_rem' [lemma, in quot_rem']
Z.quot_wd [definition, in quot_wd]
Z.quot2 [definition, in quot2]
Z.rem [definition, in rem]
Z.rem_opp_r' [lemma, in rem_opp_r']
Z.rem_opp_l [lemma, in rem_opp_l]
Z.rem_bound_pos [lemma, in rem_bound_pos]
Z.rem_wd [definition, in rem_wd]
Z.rem_opp_r [lemma, in rem_opp_r]
Z.rem_opp_l' [lemma, in rem_opp_l']
Z.sgn [definition, in sgn]
Z.sgn_pos [lemma, in sgn_pos]
Z.sgn_null [lemma, in sgn_null]
Z.sgn_neg [lemma, in sgn_neg]
Z.shiftl [definition, in shiftl]
Z.shiftl_spec_low [lemma, in shiftl_spec_low]
Z.shiftl_spec_high [lemma, in shiftl_spec_high]
Z.shiftr [definition, in shiftr]
Z.shiftr_spec_aux [lemma, in shiftr_spec_aux]
Z.shiftr_spec [lemma, in shiftr_spec]
Z.sqrt [definition, in sqrt]
Z.sqrtrem [definition, in sqrtrem]
Z.sqrtrem_sqrt [lemma, in sqrtrem_sqrt]
Z.sqrtrem_spec [lemma, in sqrtrem_spec]
Z.sqrt_spec [lemma, in sqrt_spec]
Z.sqrt_neg [lemma, in sqrt_neg]
Z.square [definition, in square]
Z.square_spec [lemma, in square_spec]
Z.sub [definition, in sub]
Z.sub_wd [definition, in sub_wd]
Z.sub_succ_r [lemma, in sub_succ_r]
Z.sub_0_r [lemma, in sub_0_r]
Z.succ [definition, in succ]
Z.succ_wd [definition, in succ_wd]
Z.succ_double [definition, in succ_double]
Z.succ_pred [lemma, in succ_pred]
Z.succ_double_spec [lemma, in succ_double_spec]
Z.t [definition, in t]
Z.testbit [definition, in testbit]
Z.testbit_even_0 [lemma, in testbit_even_0]
Z.testbit_neg_r [lemma, in testbit_neg_r]
Z.testbit_even_succ [lemma, in testbit_even_succ]
Z.testbit_0_l [lemma, in testbit_0_l]
Z.testbit_odd_0 [lemma, in testbit_odd_0]
Z.testbit_odd_succ [lemma, in testbit_odd_succ]
Z.testbit_wd [definition, in testbit_wd]
Z.to_N [definition, in to_N]
Z.to_nat [definition, in to_nat]
Z.to_pos [definition, in to_pos]
Z.two [definition, in two]
Z.two_succ [lemma, in two_succ]
Z.zero [definition, in zero]
_ < _ < _ (Z_scope) [notation, in :Z_scope:x_'<'_x_'<'_x]
_ >=? _ (Z_scope) [notation, in :Z_scope:x_'>=?'_x]
_ / _ (Z_scope) [notation, in :Z_scope:x_'/'_x]
_ > _ (Z_scope) [notation, in :Z_scope:x_'>'_x]
_ >= _ (Z_scope) [notation, in :Z_scope:x_'>='_x]
_ =? _ (Z_scope) [notation, in :Z_scope:x_'=?'_x]
_ + _ (Z_scope) [notation, in :Z_scope:x_'+'_x]
_ - _ (Z_scope) [notation, in :Z_scope:x_'-'_x]
_ ?= _ (Z_scope) [notation, in :Z_scope:x_'?='_x]
_ _ (Z_scope) [notation, in :Z_scope:x_''_x]
_ mod _ (Z_scope) [notation, in :Z_scope:x_'mod'_x]
_ ÷ _ (Z_scope) [notation, in :Z_scope:x_'÷'_x]
_ <= _ < _ (Z_scope) [notation, in :Z_scope:x_'<='_x_'<'_x]
_ <=? _ (Z_scope) [notation, in :Z_scope:x_'<=?'_x]
_ ^ _ (Z_scope) [notation, in :Z_scope:x_'^'_x]
_ < _ <= _ (Z_scope) [notation, in :Z_scope:x_'<'_x_'<='_x]
_ >? _ (Z_scope) [notation, in :Z_scope:x_'>?'_x]
_ * _ (Z_scope) [notation, in :Z_scope:x_'*'_x]
_ <= _ <= _ (Z_scope) [notation, in :Z_scope:x_'<='_x_'<='_x]
_ < _ (Z_scope) [notation, in :Z_scope:x_'<'_x]
- _ (Z_scope) [notation, in :Z_scope:'-'_x]
_ <= _ (Z_scope) [notation, in :Z_scope:x_'<='_x]
( _ | _ ) [notation, in ::'('_x_'|'_x_')']
Z0 [constructor, in Z0]
Z0 [abbreviation, in Z0]
Z2N [module, in Z2N]
Z2Nat [module, in Z2Nat]
Z2Nat.id [lemma, in id]
Z2Nat.inj [lemma, in inj]
Z2Nat.inj_max [lemma, in inj_max]
Z2Nat.inj_lt [lemma, in inj_lt]
Z2Nat.inj_pos [lemma, in inj_pos]
Z2Nat.inj_mul [lemma, in inj_mul]
Z2Nat.inj_iff [lemma, in inj_iff]
Z2Nat.inj_0 [lemma, in inj_0]
Z2Nat.inj_add [lemma, in inj_add]
Z2Nat.inj_compare [lemma, in inj_compare]
Z2Nat.inj_sub [lemma, in inj_sub]
Z2Nat.inj_min [lemma, in inj_min]
Z2Nat.inj_le [lemma, in inj_le]
Z2Nat.inj_neg [lemma, in inj_neg]
Z2Nat.inj_pred [lemma, in inj_pred]
Z2Nat.inj_succ [lemma, in inj_succ]
Z2N.id [lemma, in id]
Z2N.inj [lemma, in inj]
Z2N.inj_max [lemma, in inj_max]
Z2N.inj_lt [lemma, in inj_lt]
Z2N.inj_pos [lemma, in inj_pos]
Z2N.inj_mul [lemma, in inj_mul]
Z2N.inj_mod [lemma, in inj_mod]
Z2N.inj_iff [lemma, in inj_iff]
Z2N.inj_quot [lemma, in inj_quot]
Z2N.inj_0 [lemma, in inj_0]
Z2N.inj_add [lemma, in inj_add]
Z2N.inj_div2 [lemma, in inj_div2]
Z2N.inj_compare [lemma, in inj_compare]
Z2N.inj_sub [lemma, in inj_sub]
Z2N.inj_testbit [lemma, in inj_testbit]
Z2N.inj_min [lemma, in inj_min]
Z2N.inj_quot2 [lemma, in inj_quot2]
Z2N.inj_le [lemma, in inj_le]
Z2N.inj_neg [lemma, in inj_neg]
Z2N.inj_pred [lemma, in inj_pred]
Z2N.inj_succ [lemma, in inj_succ]
Z2N.inj_div [lemma, in inj_div]
Z2N.inj_rem [lemma, in inj_rem]
Z2N.inj_pow [lemma, in inj_pow]
Z2P [abbreviation, in Z2P]
Z2Pos [module, in Z2Pos]
Z2Pos.id [lemma, in id]
Z2Pos.inj [lemma, in inj]
Z2Pos.inj_max [lemma, in inj_max]
Z2Pos.inj_succ_double [lemma, in inj_succ_double]
Z2Pos.inj_sqrt [lemma, in inj_sqrt]
Z2Pos.inj_mul [lemma, in inj_mul]
Z2Pos.inj_double [lemma, in inj_double]
Z2Pos.inj_iff [lemma, in inj_iff]
Z2Pos.inj_leb [lemma, in inj_leb]
Z2Pos.inj_add [lemma, in inj_add]
Z2Pos.inj_gcd [lemma, in inj_gcd]
Z2Pos.inj_compare [lemma, in inj_compare]
Z2Pos.inj_sub [lemma, in inj_sub]
Z2Pos.inj_1 [lemma, in inj_1]
Z2Pos.inj_min [lemma, in inj_min]
Z2Pos.inj_ltb [lemma, in inj_ltb]
Z2Pos.inj_pred [lemma, in inj_pred]
Z2Pos.inj_succ [lemma, in inj_succ]
Z2Pos.inj_pow [lemma, in inj_pow]
Z2Pos.inj_eqb [lemma, in inj_eqb]
Z2Pos.inj_pow_pos [lemma, in inj_pow_pos]
Z2Pos.to_pos_nonpos [lemma, in to_pos_nonpos]
Z2P_correct [abbreviation, in Z2P_correct]