Z (abbreviation)
Z [in Z]
Zabs [in Zabs]
Zabs_N [in Zabs_N]
Zabs_pos [in Zabs_pos]
Zabs_triangle [in Zabs_triangle]
Zabs_nat_Zplus [in Zabs_nat_Zplus]
Zabs_Zsgn [in Zabs_Zsgn]
Zabs_N_mult_abs [in Zabs_N_mult_abs]
Zabs_N_succ_abs [in Zabs_N_succ_abs]
Zabs_N_plus [in Zabs_N_plus]
Zabs_involutive [in Zabs_involutive]
Zabs_N_succ [in Zabs_N_succ]
Zabs_non_eq [in Zabs_non_eq]
Zabs_non_eq [in Zabs_non_eq]
Zabs_of_N [in Zabs_of_N]
Zabs_nat_Zsucc [in Zabs_nat_Zsucc]
Zabs_Zopp [in Zabs_Zopp]
Zabs_nat_Z_of_nat [in Zabs_nat_Z_of_nat]
Zabs_nat_mult [in Zabs_nat_mult]
Zabs_Zmult [in Zabs_Zmult]
Zabs_nat_compare [in Zabs_nat_compare]
Zabs_nat_Zminus [in Zabs_nat_Zminus]
Zabs_square [in Zabs_square]
Zabs_N_mult [in Zabs_N_mult]
Zabs_nat [in Zabs_nat]
Zabs_eq_case [in Zabs_eq_case]
Zabs_N_plus_abs [in Zabs_N_plus_abs]
Zabs_eq [in Zabs_eq]
Zabs_eq [in Zabs_eq]
ZAddOrderProp.sub_pos [in sub_pos]
ZAddOrderProp.sub_nonneg [in sub_nonneg]
ZAddOrderProp.sub_neg [in sub_neg]
ZAddOrderProp.sub_nonpos [in sub_nonpos]
ZBitsProp.lnextcarry [in lnextcarry]
ZBitsProp.lxor3 [in lxor3]
ZBitsProp.nextcarry [in nextcarry]
ZBitsProp.xor3 [in xor3]
Zcompare [in Zcompare]
Zcompare_refl [in Zcompare_refl]
Zcompare_Eq_iff_eq [in Zcompare_Eq_iff_eq]
Zcompare_spec [in Zcompare_spec]
Zcompare_Eq_eq [in Zcompare_Eq_eq]
ZC1 [in ZC1]
ZC2 [in ZC2]
Zdiv [in Zdiv]
Zdivide [in Zdivide]
Zdivide_factor_r [in Zdivide_factor_r]
Zdivide_0 [in Zdivide_0]
Zdivide_factor_l [in Zdivide_factor_l]
Zdivide_antisym [in Zdivide_antisym]
Zdivide_1 [in Zdivide_1]
Zdivide_trans [in Zdivide_trans]
Zdivide_minus_l [in Zdivide_minus_l]
Zdivide_mult_l [in Zdivide_mult_l]
Zdivide_plus_r [in Zdivide_plus_r]
Zdivide_refl [in Zdivide_refl]
Zdivide_mult_r [in Zdivide_mult_r]
Zdiv_eucl [in Zdiv_eucl]
Zdiv_eucl_eq [in Zdiv_eucl_eq]
Zdiv_eucl_POS [in Zdiv_eucl_POS]
Zdiv2 [in Zdiv2]
Zdouble [in Zdouble]
Zdouble_mult [in Zdouble_mult]
Zdouble_plus_one [in Zdouble_plus_one]
Zdouble_minus_one [in Zdouble_minus_one]
Zdouble_plus_one_mult [in Zdouble_plus_one_mult]
Zeq_le [in Zeq_le]
ZeroSuccPredNotation.P [in P]
ZeroSuccPredNotation.S [in S]
Zeven_bool_succ [in Zeven_bool_succ]
Zeven_bool_pred [in Zeven_bool_pred]
Zeven_bool [in Zeven_bool]
Zgcd [in Zgcd]
Zgcd_nonneg [in Zgcd_nonneg]
Zgcd_is_pos [in Zgcd_is_pos]
Zgcd_comm [in Zgcd_comm]
Zgcd_greatest [in Zgcd_greatest]
Zgcd_inv_0_r [in Zgcd_inv_0_r]
Zgcd_Zabs [in Zgcd_Zabs]
Zgcd_0 [in Zgcd_0]
Zgcd_divide_r [in Zgcd_divide_r]
Zgcd_1 [in Zgcd_1]
Zgcd_divide_l [in Zgcd_divide_l]
Zgcd_inv_0_l [in Zgcd_inv_0_l]
Zge [in Zge]
Zge_bool [in Zge_bool]
Zge_le [in Zge_le]
Zge_iff_le [in Zge_iff_le]
Zggcd [in Zggcd]
Zggcd_opp [in Zggcd_opp]
Zggcd_correct_divisors [in Zggcd_correct_divisors]
Zggcd_gcd [in Zggcd_gcd]
Zgt [in Zgt]
Zgt_bool [in Zgt_bool]
Zgt_iff_lt [in Zgt_iff_lt]
Zgt_lt [in Zgt_lt]
Zind [in Zind]
Zle [in Zle]
Zle_pred [in Zle_pred]
Zle_max_r [in Zle_max_r]
Zle_ge [in Zle_ge]
Zle_bool [in Zle_bool]
Zle_0_1 [in Zle_0_1]
Zle_plus_swap [in Zle_plus_swap]
Zle_min_r [in Zle_min_r]
Zle_max_l [in Zle_max_l]
Zle_bool_refl [in Zle_bool_refl]
Zle_or_lt [in Zle_or_lt]
Zle_max_compat_r [in Zle_max_compat_r]
Zle_le_succ [in Zle_le_succ]
Zle_max_compat_l [in Zle_max_compat_l]
Zle_refl [in Zle_refl]
Zle_antisym [in Zle_antisym]
Zle_trans [in Zle_trans]
Zle_min_compat_l [in Zle_min_compat_l]
Zle_min_l [in Zle_min_l]
Zle_succ [in Zle_succ]
Zle_lt_or_eq_iff [in Zle_lt_or_eq_iff]
Zle_lt_trans [in Zle_lt_trans]
Zle_min_compat_r [in Zle_min_compat_r]
Zle_succ_l [in Zle_succ_l]
Zlt [in Zlt]
Zlt_succ [in Zlt_succ]
Zlt_irrefl [in Zlt_irrefl]
Zlt_plus_swap [in Zlt_plus_swap]
Zlt_0_1 [in Zlt_0_1]
Zlt_gt [in Zlt_gt]
Zlt_trans [in Zlt_trans]
Zlt_le_weak [in Zlt_le_weak]
Zlt_asym [in Zlt_asym]
Zlt_not_eq [in Zlt_not_eq]
Zlt_succ_r [in Zlt_succ_r]
Zlt_minus_simpl_swap [in Zlt_minus_simpl_swap]
Zlt_lt_succ [in Zlt_lt_succ]
Zlt_bool [in Zlt_bool]
Zlt_le_trans [in Zlt_le_trans]
Zlt_pred [in Zlt_pred]
Zlt_O_minus_lt [in Zlt_O_minus_lt]
ZL4 [in ZL4]
Zmax [in Zmax]
Zmax_min_modular_r [in Zmax_min_modular_r]
Zmax_irreducible_inf [in Zmax_irreducible_inf]
Zmax_comm [in Zmax_comm]
Zmax_case [in Zmax_case]
Zmax_right [in Zmax_right]
Zmax_le_prime_inf [in Zmax_le_prime_inf]
Zmax_n_n [in Zmax_n_n]
Zmax_min_distr_r [in Zmax_min_distr_r]
Zmax_assoc [in Zmax_assoc]
Zmax_le_prime [in Zmax_le_prime]
Zmax_plus [in Zmax_plus]
Zmax_lub [in Zmax_lub]
Zmax_case_strong [in Zmax_case_strong]
Zmax_l [in Zmax_l]
Zmax_lub_lt [in Zmax_lub_lt]
Zmax_idempotent [in Zmax_idempotent]
Zmax_SS [in Zmax_SS]
Zmax_min_absorption_r_r [in Zmax_min_absorption_r_r]
Zmax_irreducible_dec [in Zmax_irreducible_dec]
Zmax_r [in Zmax_r]
Zmax1 [in Zmax1]
Zmax2 [in Zmax2]
Zmin [in Zmin]
Zminus [in Zminus]
Zminus_succ_r [in Zminus_succ_r]
Zminus_plus [in Zminus_plus]
Zminus_plus_distr [in Zminus_plus_distr]
Zminus_diag [in Zminus_diag]
Zminus_0_r [in Zminus_0_r]
Zmin_idempotent [in Zmin_idempotent]
Zmin_plus [in Zmin_plus]
Zmin_max_modular_r [in Zmin_max_modular_r]
Zmin_case_strong [in Zmin_case_strong]
Zmin_max_absorption_r_r [in Zmin_max_absorption_r_r]
Zmin_max_distr_r [in Zmin_max_distr_r]
Zmin_case [in Zmin_case]
Zmin_comm [in Zmin_comm]
Zmin_glb [in Zmin_glb]
Zmin_r [in Zmin_r]
Zmin_glb_lt [in Zmin_glb_lt]
Zmin_or [in Zmin_or]
Zmin_irreducible_inf [in Zmin_irreducible_inf]
Zmin_SS [in Zmin_SS]
Zmin_assoc [in Zmin_assoc]
Zmin_n_n [in Zmin_n_n]
Zmin_l [in Zmin_l]
Zmod [in Zmod]
Zmod_pos_bound [in Zmod_pos_bound]
Zmod_POS_bound [in Zmod_POS_bound]
Zmod_neg_bound [in Zmod_neg_bound]
ZMulOrderProp.le_0_square [in le_0_square]
ZMulOrderProp.mul_nonneg [in mul_nonneg]
ZMulOrderProp.mul_pos [in mul_pos]
ZMulOrderProp.mul_nonpos [in mul_nonpos]
ZMulOrderProp.mul_neg [in mul_neg]
Zmult [in Zmult]
Zmult_assoc [in Zmult_assoc]
Zmult_succ_l [in Zmult_succ_l]
Zmult_1_r [in Zmult_1_r]
Zmult_divide_compat_r [in Zmult_divide_compat_r]
Zmult_reg_l [in Zmult_reg_l]
Zmult_divide_compat_l [in Zmult_divide_compat_l]
Zmult_0_l [in Zmult_0_l]
Zmult_reg_r [in Zmult_reg_r]
Zmult_comm [in Zmult_comm]
Zmult_succ_r [in Zmult_succ_r]
Zmult_1_l [in Zmult_1_l]
Zmult_1_inversion_l [in Zmult_1_inversion_l]
Zmult_0_r [in Zmult_0_r]
Zmult_lt_0_compat [in Zmult_lt_0_compat]
Zmult_permute [in Zmult_permute]
Zmult_le_0_compat [in Zmult_le_0_compat]
Zmult_lt_O_compat [in Zmult_lt_O_compat]
Zmult_plus_distr_r [in Zmult_plus_distr_r]
Zmult_opp_comm [in Zmult_opp_comm]
Zmult_minus_distr_r [in Zmult_minus_distr_r]
Zmult_opp_opp [in Zmult_opp_opp]
Zmult_plus_distr_l [in Zmult_plus_distr_l]
Zneg [in Zneg]
Zneg_xI [in Zneg_xI]
Zneg_xO [in Zneg_xO]
Zneg_plus_distr [in Zneg_plus_distr]
Zodd_bool_pred [in Zodd_bool_pred]
Zodd_bool [in Zodd_bool]
Zodd_bool_succ [in Zodd_bool_succ]
ZOdiv [in ZOdiv]
ZOdiv_lt_upper_bound [in ZOdiv_lt_upper_bound]
ZOdiv_le_lower_bound [in ZOdiv_le_lower_bound]
ZOdiv_mult_cancel_l [in ZOdiv_mult_cancel_l]
ZOdiv_eucl_correct [in ZOdiv_eucl_correct]
ZOdiv_opp_opp [in ZOdiv_opp_opp]
ZOdiv_le_upper_bound [in ZOdiv_le_upper_bound]
ZOdiv_small [in ZOdiv_small]
ZOdiv_unique_full [in ZOdiv_unique_full]
ZOdiv_mult_cancel_r [in ZOdiv_mult_cancel_r]
ZOdiv_mult_le [in ZOdiv_mult_le]
ZOdiv_ZOdiv [in ZOdiv_ZOdiv]
ZOdiv_1_l [in ZOdiv_1_l]
ZOdiv_mod_unique_full [in ZOdiv_mod_unique_full]
ZOdiv_eucl_Zdiv_eucl_pos [in ZOdiv_eucl_Zdiv_eucl_pos]
ZOdiv_0_l [in ZOdiv_0_l]
ZOdiv_opp_l [in ZOdiv_opp_l]
ZOdiv_1_r [in ZOdiv_1_r]
ZOdiv_eucl [in ZOdiv_eucl]
ZOdiv_sgn [in ZOdiv_sgn]
ZOdiv_opp_r [in ZOdiv_opp_r]
ZOdiv_unique [in ZOdiv_unique]
ZOdiv_Zdiv_pos [in ZOdiv_Zdiv_pos]
ZOdiv_0_r [in ZOdiv_0_r]
ZOmod [in ZOmod]
ZOmod_lt_neg_pos [in ZOmod_lt_neg_pos]
ZOmod_sgn2 [in ZOmod_sgn2]
ZOmod_sgn [in ZOmod_sgn]
ZOmod_Zmod_pos [in ZOmod_Zmod_pos]
ZOmod_opp_opp [in ZOmod_opp_opp]
ZOmod_0_r [in ZOmod_0_r]
ZOmod_lt_pos [in ZOmod_lt_pos]
ZOmod_opp_r [in ZOmod_opp_r]
ZOmod_divides [in ZOmod_divides]
ZOmod_lt_pos_neg [in ZOmod_lt_pos_neg]
ZOmod_unique_full [in ZOmod_unique_full]
ZOmod_Zmod_zero [in ZOmod_Zmod_zero]
ZOmod_lt_pos_pos [in ZOmod_lt_pos_pos]
ZOmod_1_r [in ZOmod_1_r]
ZOmod_lt_neg_neg [in ZOmod_lt_neg_neg]
ZOmod_small [in ZOmod_small]
ZOmod_opp_l [in ZOmod_opp_l]
ZOmod_mod [in ZOmod_mod]
ZOmod_0_l [in ZOmod_0_l]
ZOmod_le [in ZOmod_le]
ZOmod_lt [in ZOmod_lt]
ZOmod_unique [in ZOmod_unique]
ZOmod_lt_neg [in ZOmod_lt_neg]
ZOmod_1_l [in ZOmod_1_l]
ZOmult_mod_distr_l [in ZOmult_mod_distr_l]
ZOmult_mod_idemp_r [in ZOmult_mod_idemp_r]
ZOmult_mod_idemp_l [in ZOmult_mod_idemp_l]
ZOmult_mod [in ZOmult_mod]
ZOmult_mod_distr_r [in ZOmult_mod_distr_r]
Zone_divide [in Zone_divide]
ZOplus_mod_idemp_l [in ZOplus_mod_idemp_l]
ZOplus_mod_idemp_r [in ZOplus_mod_idemp_r]
ZOplus_mod [in ZOplus_mod]
Zopp [in Zopp]
Zopp_involutive [in Zopp_involutive]
Zopp_neg [in Zopp_neg]
Zopp_0 [in Zopp_0]
Zopp_succ [in Zopp_succ]
Zopp_mult_distr_l_reverse [in Zopp_mult_distr_l_reverse]
Zopp_plus_distr [in Zopp_plus_distr]
Zopp_inj [in Zopp_inj]
Zopp_eq_mult_neg_1 [in Zopp_eq_mult_neg_1]
ZO_mult_div_ge [in ZO_mult_div_ge]
ZO_mod_mult [in ZO_mod_mult]
ZO_mult_div_le [in ZO_mult_div_le]
ZO_div_plus_l [in ZO_div_plus_l]
ZO_div_monotone [in ZO_div_monotone]
ZO_div_same [in ZO_div_same]
ZO_div_lt [in ZO_div_lt]
ZO_mod_same [in ZO_mod_same]
ZO_div_mod_eq [in ZO_div_mod_eq]
ZO_mod_plus [in ZO_mod_plus]
ZO_div_pos [in ZO_div_pos]
ZO_div_mult [in ZO_div_mult]
ZO_div_plus [in ZO_div_plus]
Zplus [in Zplus]
Zplus_0_l [in Zplus_0_l]
Zplus_permute [in Zplus_permute]
Zplus_lt_le_compat [in Zplus_lt_le_compat]
Zplus_comm [in Zplus_comm]
Zplus_opp_r [in Zplus_opp_r]
Zplus_0_r [in Zplus_0_r]
Zplus_le_0_compat [in Zplus_le_0_compat]
Zplus_succ_l [in Zplus_succ_l]
Zplus_opp_l [in Zplus_opp_l]
Zplus_max_distr_r [in Zplus_max_distr_r]
Zplus_le_lt_compat [in Zplus_le_lt_compat]
Zplus_succ_r [in Zplus_succ_r]
Zplus_le_compat [in Zplus_le_compat]
Zplus_max_distr_l [in Zplus_max_distr_l]
Zplus_min_distr_r [in Zplus_min_distr_r]
Zplus_lt_compat [in Zplus_lt_compat]
Zplus_assoc [in Zplus_assoc]
Zplus_reg_l [in Zplus_reg_l]
Zplus_succ_comm [in Zplus_succ_comm]
Zplus' [in Zplus']
ZPminus [in ZPminus]
Zpos [in Zpos]
Zpos_xI [in Zpos_xI]
Zpos_minus [in Zpos_minus]
Zpos_min [in Zpos_min]
Zpos_eq_Z_of_nat_o_nat_of_P [in Zpos_eq_Z_of_nat_o_nat_of_P]
Zpos_xO [in Zpos_xO]
Zpos_eq_rev [in Zpos_eq_rev]
Zpos_max [in Zpos_max]
Zpos_minus_morphism [in Zpos_minus_morphism]
Zpos_plus_distr [in Zpos_plus_distr]
Zpos_succ_morphism [in Zpos_succ_morphism]
Zpos_mult_morphism [in Zpos_mult_morphism]
Zpower [in Zpower]
Zpower_1_l [in Zpower_1_l]
Zpower_neg_r [in Zpower_neg_r]
Zpower_0_r [in Zpower_0_r]
Zpower_0_r [in Zpower_0_r]
Zpower_nat_Zpower [in Zpower_nat_Zpower]
Zpower_le_monotone2 [in Zpower_le_monotone2]
Zpower_pos [in Zpower_pos]
Zpower_1_r [in Zpower_1_r]
Zpower_2 [in Zpower_2]
Zpower_Ppow [in Zpower_Ppow]
Zpower_mult [in Zpower_mult]
Zpower_gt_0 [in Zpower_gt_0]
Zpower_ge_0 [in Zpower_ge_0]
Zpower_0_l [in Zpower_0_l]
Zpower_succ_r [in Zpower_succ_r]
Zpower_Zsucc [in Zpower_Zsucc]
Zpower_Zabs [in Zpower_Zabs]
Zpred [in Zpred]
Zpred' [in Zpred']
Zpred'_succ' [in Zpred'_succ']
Zpred'_inj [in Zpred'_inj]
Zquot_unique [in Zquot_unique]
Zquot_1_l [in Zquot_1_l]
Zquot_1_r [in Zquot_1_r]
Zquot_small [in Zquot_small]
Zquot2 [in Zquot2]
Zquot2_quot [in Zquot2_quot]
Zrem_1_r [in Zrem_1_r]
Zrem_small [in Zrem_small]
Zrem_1_l [in Zrem_1_l]
Zrem_lt [in Zrem_lt]
Zrem_unique [in Zrem_unique]
Zsgn [in Zsgn]
Zsgn_m1 [in Zsgn_m1]
Zsgn_Zabs [in Zsgn_Zabs]
Zsgn_Zmult [in Zsgn_Zmult]
Zsgn_Zopp [in Zsgn_Zopp]
Zsgn_neg [in Zsgn_neg]
Zsgn_pos [in Zsgn_pos]
Zsgn_0 [in Zsgn_0]
Zsgn_null [in Zsgn_null]
Zsgn_1 [in Zsgn_1]
Zsquare [in Zsquare]
Zsquare_correct [in Zsquare_correct]
Zsucc [in Zsucc]
Zsucc_max_distr [in Zsucc_max_distr]
Zsucc_inj [in Zsucc_inj]
Zsucc_discr [in Zsucc_discr]
Zsucc_min_distr [in Zsucc_min_distr]
Zsucc' [in Zsucc']
Zsucc'_pred' [in Zsucc'_pred']
Zsucc'_inj [in Zsucc'_inj]
Zsucc'_discr [in Zsucc'_discr]
Z_of_N_gt_iff [in Z_of_N_gt_iff]
Z_of_N_plus [in Z_of_N_plus]
Z_eq_dec [in Z_eq_dec]
Z_of_N_gt_rev [in Z_of_N_gt_rev]
Z_of_nat_of_N [in Z_of_nat_of_N]
Z_rect [in Z_rect]
Z_of_N_eq [in Z_of_N_eq]
Z_of_N_le_rev [in Z_of_N_le_rev]
Z_of_N [in Z_of_N]
Z_of_N_le_iff [in Z_of_N_le_iff]
Z_of_N_pos [in Z_of_N_pos]
Z_of_N_ge [in Z_of_N_ge]
Z_quot_mult [in Z_quot_mult]
Z_quot_same [in Z_quot_same]
Z_of_N_le_0 [in Z_of_N_le_0]
Z_of_nat_of_P [in Z_of_nat_of_P]
Z_of_N_ge_rev [in Z_of_N_ge_rev]
Z_of_N_min [in Z_of_N_min]
Z_of_N_eq_rev [in Z_of_N_eq_rev]
Z_of_N_lt_rev [in Z_of_N_lt_rev]
Z_of_N_lt_iff [in Z_of_N_lt_iff]
Z_of_N_abs [in Z_of_N_abs]
Z_ind [in Z_ind]
Z_of_N_ge_iff [in Z_of_N_ge_iff]
Z_of_N_eq_iff [in Z_of_N_eq_iff]
Z_of_nat [in Z_of_nat]
Z_of_N_lt [in Z_of_N_lt]
Z_of_N_mult [in Z_of_N_mult]
Z_quot_rem_eq [in Z_quot_rem_eq]
Z_of_N_le [in Z_of_N_le]
Z_of_N_minus [in Z_of_N_minus]
Z_rec [in Z_rec]
Z_of_N_succ [in Z_of_N_succ]
Z_of_N_compare [in Z_of_N_compare]
Z_of_N_of_nat [in Z_of_N_of_nat]
Z_div_mod_eq_full [in Z_div_mod_eq_full]
Z_of_N_gt [in Z_of_N_gt]
Z_of_N_max [in Z_of_N_max]
Z.neg [in neg]
Z.pos [in pos]
Z0 [in Z0]
Z2P [in Z2P]
Z2P_correct [in Z2P_correct]