Coq.ZArith.Zwf

Global Index

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)

Z (lemma)

Zabs_eq [in Coq.ZArith.Zabs]
Zabs_eq_case [in Coq.ZArith.Zabs]
Zabs_ind [in Coq.ZArith.Zabs]
Zabs_intro [in Coq.ZArith.Zabs]
Zabs_nat_lt [in Coq.ZArith.Zabs]
Zabs_non_eq [in Coq.ZArith.Zabs]
Zabs_pos [in Coq.ZArith.Zabs]
Zabs_triangle [in Coq.ZArith.Zabs]
Zabs_Zmult [in Coq.ZArith.Zabs]
Zabs_Zopp [in Coq.ZArith.Zabs]
Zabs_Zsgn [in Coq.ZArith.Zabs]
Zcase_sign [in Coq.ZArith.Zcomplements]
Zcompare_antisym [in Coq.ZArith.Zcompare]
Zcompare_egal_dec [in Coq.ZArith.Zcompare]
Zcompare_elim [in Coq.ZArith.Zcompare]
Zcompare_eq_case [in Coq.ZArith.Zcompare]
Zcompare_Eq_eq [in Coq.ZArith.Zcompare]
Zcompare_Eq_iff_eq [in Coq.ZArith.Zcompare]
Zcompare_Gt_Lt_antisym [in Coq.ZArith.Zcompare]
Zcompare_Gt_not_Lt [in Coq.ZArith.Zcompare]
Zcompare_Gt_spec [in Coq.ZArith.Zcompare]
Zcompare_Gt_trans [in Coq.ZArith.Zcompare]
Zcompare_mult_compat [in Coq.ZArith.Zcompare]
Zcompare_opp [in Coq.ZArith.Zcompare]
Zcompare_plus_compat [in Coq.ZArith.Zcompare]
Zcompare_rec [in Coq.ZArith.ZArith_dec]
Zcompare_refl [in Coq.ZArith.Zcompare]
Zcompare_succ_compat [in Coq.ZArith.Zcompare]
Zcompare_succ_Gt [in Coq.ZArith.Zcompare]
ZC1 [in Coq.NArith.BinPos]
ZC2 [in Coq.NArith.BinPos]
ZC3 [in Coq.NArith.BinPos]
ZC4 [in Coq.NArith.BinPos]
Zdivide_antisym [in Coq.ZArith.Znumtheory]
Zdivide_bounds [in Coq.ZArith.Znumtheory]
Zdivide_dec [in Coq.ZArith.Znumtheory]
Zdivide_factor_l [in Coq.ZArith.Znumtheory]
Zdivide_factor_r [in Coq.ZArith.Znumtheory]
Zdivide_minus_l [in Coq.ZArith.Znumtheory]
Zdivide_mod [in Coq.ZArith.Znumtheory]
Zdivide_mult_l [in Coq.ZArith.Znumtheory]
Zdivide_mult_r [in Coq.ZArith.Znumtheory]
Zdivide_opp_l [in Coq.ZArith.Znumtheory]
Zdivide_opp_l_rev [in Coq.ZArith.Znumtheory]
Zdivide_opp_r [in Coq.ZArith.Znumtheory]
Zdivide_opp_r_rev [in Coq.ZArith.Znumtheory]
Zdivide_plus_r [in Coq.ZArith.Znumtheory]
Zdivide_refl [in Coq.ZArith.Znumtheory]
Zdivide_0 [in Coq.ZArith.Znumtheory]
Zdivide_1 [in Coq.ZArith.Znumtheory]
Zdiv2_two_power_nat [in Coq.ZArith.Zbinary]
Zdiv_eucl_exist [in Coq.ZArith.Zdiv]
Zdiv_eucl_extended [in Coq.ZArith.Zdiv]
Zdiv_rest_correct [in Coq.ZArith.Zpower]
Zdiv_rest_correct1 [in Coq.ZArith.Zpower]
Zdiv_rest_correct2 [in Coq.ZArith.Zpower]
Zegal_left [in Coq.ZArith.auxiliary]
Zeq_le [in Coq.ZArith.Zorder]
Zeq_minus [in Coq.ZArith.BinInt]
Zeq_plus_swap [in Coq.ZArith.Zorder]
zerob_false_elim [in Coq.Bool.Zerob]
zerob_false_intro [in Coq.Bool.Zerob]
zerob_true_elim [in Coq.Bool.Zerob]
zerob_true_intro [in Coq.Bool.Zerob]
ZERO_le_N_digits [in Coq.ZArith.Zlogarithm]
Zeven_bit_value [in Coq.ZArith.Zbinary]
Zeven_div2 [in Coq.ZArith.Zeven]
Zeven_not_Zodd [in Coq.ZArith.Zeven]
Zeven_pred [in Coq.ZArith.Zeven]
Zeven_Sn [in Coq.ZArith.Zeven]
Zgcd_is_gcd [in Coq.ZArith.Znumtheory]
Zgcd_is_pos [in Coq.ZArith.Znumtheory]
Zgcd_spec [in Coq.ZArith.Znumtheory]
Zge_cases [in Coq.ZArith.Zbool]
Zge_compare [in Coq.ZArith.Zcompare]
Zge_iff_le [in Coq.ZArith.Zorder]
Zge_is_le_bool [in Coq.ZArith.Zbool]
Zge_le [in Coq.ZArith.Zorder]
Zge_left [in Coq.ZArith.auxiliary]
Zge_minus_two_power_nat_S [in Coq.ZArith.Zbinary]
Zge_trans [in Coq.ZArith.Zorder]
Zge_trans_succ [in Coq.ZArith.Zorder]
Zggcd_correct_divisors [in Coq.ZArith.Znumtheory]
Zggcd_gcd [in Coq.ZArith.Znumtheory]
Zgt_asym [in Coq.ZArith.Zorder]
Zgt_cases [in Coq.ZArith.Zbool]
Zgt_compare [in Coq.ZArith.Zcompare]
Zgt_iff_lt [in Coq.ZArith.Zorder]
Zgt_irrefl [in Coq.ZArith.Zorder]
Zgt_is_le_bool [in Coq.ZArith.Zbool]
Zgt_left [in Coq.ZArith.auxiliary]
Zgt_left_gt [in Coq.ZArith.auxiliary]
Zgt_left_rev [in Coq.ZArith.auxiliary]
Zgt_le_succ [in Coq.ZArith.Zorder]
Zgt_le_trans [in Coq.ZArith.Zorder]
Zgt_lt [in Coq.ZArith.Zorder]
Zgt_not_le [in Coq.ZArith.Zorder]
Zgt_pos_0 [in Coq.ZArith.Zorder]
Zgt_square_simpl [in Coq.ZArith.Zorder]
Zgt_succ [in Coq.ZArith.Zorder]
Zgt_succ_gt_or_eq [in Coq.ZArith.Zorder]
Zgt_succ_le [in Coq.ZArith.Zorder]
Zgt_succ_pred [in Coq.ZArith.Zorder]
Zgt_trans [in Coq.ZArith.Zorder]
Zgt_0_le_0_pred [in Coq.ZArith.Zorder]
Zind [in Coq.ZArith.BinInt]
Zis_gcd_bezout [in Coq.ZArith.Znumtheory]
Zis_gcd_even_odd [in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid [in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid2 [in Coq.ZArith.Znumtheory]
Zis_gcd_minus [in Coq.ZArith.Znumtheory]
Zis_gcd_mult [in Coq.ZArith.Znumtheory]
Zis_gcd_opp [in Coq.ZArith.Znumtheory]
Zis_gcd_refl [in Coq.ZArith.Znumtheory]
Zis_gcd_rel_prime [in Coq.ZArith.Znumtheory]
Zis_gcd_sym [in Coq.ZArith.Znumtheory]
Zis_gcd_uniqueness_apart_sign [in Coq.ZArith.Znumtheory]
Zis_gcd_0 [in Coq.ZArith.Znumtheory]
Zis_gcd_0_abs [in Coq.ZArith.Znumtheory]
Zis_gcd_1 [in Coq.ZArith.Znumtheory]
Zlength_cons [in Coq.ZArith.Zcomplements]
Zlength_correct [in Coq.ZArith.Zcomplements]
Zlength_nil [in Coq.ZArith.Zcomplements]
Zlength_nil_inv [in Coq.ZArith.Zcomplements]
Zle_antisym [in Coq.ZArith.Zorder]
Zle_bool_antisym [in Coq.ZArith.Zbool]
Zle_bool_imp_le [in Coq.ZArith.Zbool]
Zle_bool_plus_mono [in Coq.ZArith.Zbool]
Zle_bool_refl [in Coq.ZArith.Zbool]
Zle_bool_trans [in Coq.ZArith.Zbool]
Zle_cases [in Coq.ZArith.Zbool]
Zle_compare [in Coq.ZArith.Zcompare]
Zle_ge [in Coq.ZArith.Zorder]
Zle_gt_trans [in Coq.ZArith.Zorder]
Zle_imp_le_bool [in Coq.ZArith.Zbool]
Zle_is_le_bool [in Coq.ZArith.Zbool]
Zle_left [in Coq.ZArith.auxiliary]
Zle_left_rev [in Coq.ZArith.auxiliary]
Zle_le_succ [in Coq.ZArith.Zorder]
Zle_lt_or_eq [in Coq.ZArith.Zorder]
Zle_lt_succ [in Coq.ZArith.Zorder]
Zle_lt_trans [in Coq.ZArith.Zorder]
Zle_max_l [in Coq.ZArith.Zmax]
Zle_max_r [in Coq.ZArith.Zmax]
Zle_minus_le_0 [in Coq.ZArith.Zorder]
Zle_min_l [in Coq.ZArith.Zmin]
Zle_min_r [in Coq.ZArith.Zmin]
Zle_mult_approx [in Coq.ZArith.auxiliary]
Zle_neg_pos [in Coq.ZArith.Zorder]
Zle_not_gt [in Coq.ZArith.Zorder]
Zle_not_lt [in Coq.ZArith.Zorder]
Zle_or_lt [in Coq.ZArith.Zorder]
Zle_plus_swap [in Coq.ZArith.Zorder]
Zle_pred [in Coq.ZArith.Zorder]
Zle_refl [in Coq.ZArith.Zorder]
Zle_succ [in Coq.ZArith.Zorder]
Zle_succ_le [in Coq.ZArith.Zorder]
Zle_trans [in Coq.ZArith.Zorder]
Zle_0_minus_le [in Coq.ZArith.Zorder]
Zle_0_nat [in Coq.ZArith.Zorder]
Zle_0_pos [in Coq.ZArith.Zorder]
Zle_0_1 [in Coq.ZArith.Zorder]
Zlt_asym [in Coq.ZArith.Zorder]
Zlt_cases [in Coq.ZArith.Zbool]
Zlt_compare [in Coq.ZArith.Zcompare]
Zlt_cotrans [in Coq.ZArith.ZArith_dec]
Zlt_cotrans_neg [in Coq.ZArith.ZArith_dec]
Zlt_cotrans_pos [in Coq.ZArith.ZArith_dec]
Zlt_gt [in Coq.ZArith.Zorder]
Zlt_gt_succ [in Coq.ZArith.Zorder]
Zlt_irrefl [in Coq.ZArith.Zorder]
Zlt_is_le_bool [in Coq.ZArith.Zbool]
Zlt_left [in Coq.ZArith.auxiliary]
Zlt_left_lt [in Coq.ZArith.auxiliary]
Zlt_left_rev [in Coq.ZArith.auxiliary]
Zlt_le_succ [in Coq.ZArith.Zorder]
Zlt_le_trans [in Coq.ZArith.Zorder]
Zlt_le_weak [in Coq.ZArith.Zorder]
Zlt_lower_bound_ind [in Coq.ZArith.Wf_Z]
Zlt_lower_bound_rec [in Coq.ZArith.Wf_Z]
Zlt_lt_double [in Coq.ZArith.Zpower]
Zlt_lt_succ [in Coq.ZArith.Zorder]
Zlt_minus_simpl_swap [in Coq.ZArith.Zorder]
Zlt_neg_0 [in Coq.ZArith.Zorder]
Zlt_not_eq [in Coq.ZArith.Zorder]
Zlt_not_le [in Coq.ZArith.Zorder]
Zlt_plus_swap [in Coq.ZArith.Zorder]
Zlt_pred [in Coq.ZArith.Zorder]
Zlt_square_simpl [in Coq.ZArith.Zorder]
Zlt_succ [in Coq.ZArith.Zorder]
Zlt_succ_gt [in Coq.ZArith.Zorder]
Zlt_succ_le [in Coq.ZArith.Zorder]
Zlt_succ_pred [in Coq.ZArith.Zorder]
Zlt_trans [in Coq.ZArith.Zorder]
Zlt_two_power_nat_S [in Coq.ZArith.Zbinary]
Zlt_0_ind [in Coq.ZArith.Wf_Z]
Zlt_0_le_0_pred [in Coq.ZArith.Zorder]
Zlt_0_minus_lt [in Coq.ZArith.Zorder]
Zlt_0_rec [in Coq.ZArith.Wf_Z]
Zlt_0_1 [in Coq.ZArith.Zorder]
ZL0 [in Coq.ZArith.BinInt]
ZL10 [in Coq.NArith.BinPos]
ZL11 [in Coq.NArith.BinPos]
ZL16 [in Coq.NArith.Pnat]
ZL17 [in Coq.NArith.Pnat]
ZL3 [in Coq.NArith.Pnat]
ZL4 [in Coq.NArith.Pnat]
ZL4_inf [in Coq.ZArith.Wf_Z]
ZL5 [in Coq.NArith.Pnat]
ZL6 [in Coq.NArith.Pnat]
ZL7 [in Coq.NArith.Pnat]
ZL8 [in Coq.NArith.Pnat]
Zmax_assoc [in Coq.ZArith.Zmax]
Zmax_case [in Coq.ZArith.Zmax]
Zmax_case_strong [in Coq.ZArith.Zmax]
Zmax_comm [in Coq.ZArith.Zmax]
Zmax_idempotent [in Coq.ZArith.Zmax]
Zmax_irreducible_inf [in Coq.ZArith.Zmax]
Zmax_le_prime_inf [in Coq.ZArith.Zmax]
Zmax_lub [in Coq.ZArith.Zmax]
Zmax_min_absorption_r_r [in Coq.ZArith.Zminmax]
Zmax_min_distr_r [in Coq.ZArith.Zminmax]
Zmax_min_modular_r [in Coq.ZArith.Zminmax]
Zminus_diag [in Coq.ZArith.BinInt]
Zminus_diag_reverse [in Coq.ZArith.BinInt]
Zminus_eq [in Coq.ZArith.BinInt]
Zminus_plus [in Coq.ZArith.BinInt]
Zminus_plus_simpl_l [in Coq.ZArith.BinInt]
Zminus_plus_simpl_l_reverse [in Coq.ZArith.BinInt]
Zminus_plus_simpl_r [in Coq.ZArith.BinInt]
Zminus_succ_l [in Coq.ZArith.BinInt]
Zminus_0_l_reverse [in Coq.ZArith.BinInt]
Zminus_0_r [in Coq.ZArith.BinInt]
Zmin_assoc [in Coq.ZArith.Zmin]
Zmin_case [in Coq.ZArith.Zmin]
Zmin_case_strong [in Coq.ZArith.Zmin]
Zmin_comm [in Coq.ZArith.Zmin]
Zmin_glb [in Coq.ZArith.Zmin]
Zmin_idempotent [in Coq.ZArith.Zmin]
Zmin_irreducible [in Coq.ZArith.Zmin]
Zmin_irreducible_inf [in Coq.ZArith.Zmin]
Zmin_le_prime_inf [in Coq.ZArith.Zmin]
Zmin_max_absorption_r_r [in Coq.ZArith.Zminmax]
Zmin_max_distr_r [in Coq.ZArith.Zminmax]
Zmin_max_modular_r [in Coq.ZArith.Zminmax]
Zmod2_twice [in Coq.ZArith.Zbinary]
Zmod_divide [in Coq.ZArith.Znumtheory]
Zmult_assoc [in Coq.ZArith.BinInt]
Zmult_assoc_reverse [in Coq.ZArith.BinInt]
Zmult_comm [in Coq.ZArith.BinInt]
Zmult_compare_compat_l [in Coq.ZArith.Zcompare]
Zmult_compare_compat_r [in Coq.ZArith.Zcompare]
Zmult_divide_compat_l [in Coq.ZArith.Znumtheory]
Zmult_divide_compat_r [in Coq.ZArith.Znumtheory]
Zmult_ge_compat [in Coq.ZArith.Zorder]
Zmult_ge_compat_l [in Coq.ZArith.Zorder]
Zmult_ge_compat_r [in Coq.ZArith.Zorder]
Zmult_ge_reg_r [in Coq.ZArith.Zorder]
Zmult_gt_compat_l [in Coq.ZArith.Zorder]
Zmult_gt_compat_r [in Coq.ZArith.Zorder]
Zmult_gt_reg_r [in Coq.ZArith.Zorder]
Zmult_gt_0_compat [in Coq.ZArith.Zorder]
Zmult_gt_0_le_compat_r [in Coq.ZArith.Zorder]
Zmult_gt_0_le_0_compat [in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_l [in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_r [in Coq.ZArith.Zorder]
Zmult_gt_0_lt_reg_r [in Coq.ZArith.Zorder]
Zmult_gt_0_lt_0_reg_r [in Coq.ZArith.Zorder]
Zmult_gt_0_reg_l [in Coq.ZArith.Zorder]
Zmult_integral [in Coq.ZArith.BinInt]
Zmult_integral_l [in Coq.ZArith.BinInt]
Zmult_le_approx [in Coq.ZArith.auxiliary]
Zmult_le_compat [in Coq.ZArith.Zorder]
Zmult_le_compat_l [in Coq.ZArith.Zorder]
Zmult_le_compat_r [in Coq.ZArith.Zorder]
Zmult_le_reg_r [in Coq.ZArith.Zorder]
Zmult_le_0_compat [in Coq.ZArith.Zorder]
Zmult_le_0_reg_r [in Coq.ZArith.Zorder]
Zmult_lt_compat_l [in Coq.ZArith.Zorder]
Zmult_lt_compat_r [in Coq.ZArith.Zorder]
Zmult_lt_reg_r [in Coq.ZArith.Zorder]
Zmult_lt_0_compat [in Coq.ZArith.Zorder]
Zmult_lt_0_le_compat_r [in Coq.ZArith.Zorder]
Zmult_lt_0_le_reg_r [in Coq.ZArith.Zorder]
Zmult_lt_0_reg_r [in Coq.ZArith.Zorder]
Zmult_minus_distr_l [in Coq.ZArith.BinInt]
Zmult_minus_distr_r [in Coq.ZArith.BinInt]
Zmult_one [in Coq.ZArith.Znumtheory]
Zmult_opp_comm [in Coq.ZArith.BinInt]
Zmult_opp_opp [in Coq.ZArith.BinInt]
Zmult_permute [in Coq.ZArith.BinInt]
Zmult_plus_distr_l [in Coq.ZArith.BinInt]
Zmult_plus_distr_r [in Coq.ZArith.BinInt]
Zmult_reg_l [in Coq.ZArith.BinInt]
Zmult_reg_r [in Coq.ZArith.BinInt]
Zmult_succ_l [in Coq.ZArith.BinInt]
Zmult_succ_l_reverse [in Coq.ZArith.BinInt]
Zmult_succ_r [in Coq.ZArith.BinInt]
Zmult_succ_r_reverse [in Coq.ZArith.BinInt]
Zmult_0_l [in Coq.ZArith.BinInt]
Zmult_0_r [in Coq.ZArith.BinInt]
Zmult_0_r_reverse [in Coq.ZArith.BinInt]
Zmult_1_inversion_l [in Coq.ZArith.BinInt]
Zmult_1_l [in Coq.ZArith.BinInt]
Zmult_1_r [in Coq.ZArith.BinInt]
Zneg_plus_distr [in Coq.ZArith.BinInt]
Zneg_xI [in Coq.ZArith.BinInt]
Zneg_xO [in Coq.ZArith.BinInt]
Zne_left [in Coq.ZArith.auxiliary]
Znot_ge_lt [in Coq.ZArith.Zorder]
Znot_gt_le [in Coq.ZArith.Zorder]
Znot_le_gt [in Coq.ZArith.Zorder]
Znot_le_succ [in Coq.ZArith.Zorder]
Znot_lt_ge [in Coq.ZArith.Zorder]
Zodd_bit_value [in Coq.ZArith.Zbinary]
Zodd_div2 [in Coq.ZArith.Zeven]
Zodd_div2_neg [in Coq.ZArith.Zeven]
Zodd_not_Zeven [in Coq.ZArith.Zeven]
Zodd_pred [in Coq.ZArith.Zeven]
Zodd_Sn [in Coq.ZArith.Zeven]
Zone_divide [in Coq.ZArith.Znumtheory]
Zone_min_pos [in Coq.ZArith.Zbool]
Zone_pos [in Coq.ZArith.Zbool]
Zopp_eq_mult_neg_1 [in Coq.ZArith.BinInt]
Zopp_inj [in Coq.ZArith.BinInt]
Zopp_involutive [in Coq.ZArith.BinInt]
Zopp_mult_distr_l [in Coq.ZArith.BinInt]
Zopp_mult_distr_l_reverse [in Coq.ZArith.BinInt]
Zopp_mult_distr_r [in Coq.ZArith.BinInt]
Zopp_neg [in Coq.ZArith.BinInt]
Zopp_plus_distr [in Coq.ZArith.BinInt]
Zplus_assoc [in Coq.ZArith.BinInt]
Zplus_assoc_reverse [in Coq.ZArith.BinInt]
Zplus_comm [in Coq.ZArith.BinInt]
Zplus_compare_compat [in Coq.ZArith.Zcompare]
Zplus_diag_eq_mult_2 [in Coq.ZArith.BinInt]
Zplus_eq_compat [in Coq.ZArith.BinInt]
Zplus_gt_compat_l [in Coq.ZArith.Zorder]
Zplus_gt_compat_r [in Coq.ZArith.Zorder]
Zplus_gt_reg_l [in Coq.ZArith.Zorder]
Zplus_gt_reg_r [in Coq.ZArith.Zorder]
Zplus_le_compat [in Coq.ZArith.Zorder]
Zplus_le_compat_l [in Coq.ZArith.Zorder]
Zplus_le_compat_r [in Coq.ZArith.Zorder]
Zplus_le_lt_compat [in Coq.ZArith.Zorder]
Zplus_le_reg_l [in Coq.ZArith.Zorder]
Zplus_le_reg_r [in Coq.ZArith.Zorder]
Zplus_le_0_compat [in Coq.ZArith.Zorder]
Zplus_lt_compat [in Coq.ZArith.Zorder]
Zplus_lt_compat_l [in Coq.ZArith.Zorder]
Zplus_lt_compat_r [in Coq.ZArith.Zorder]
Zplus_lt_le_compat [in Coq.ZArith.Zorder]
Zplus_lt_reg_l [in Coq.ZArith.Zorder]
Zplus_lt_reg_r [in Coq.ZArith.Zorder]
Zplus_max_distr_r [in Coq.ZArith.Zmax]
Zplus_minus [in Coq.ZArith.BinInt]
Zplus_minus_eq [in Coq.ZArith.BinInt]
Zplus_min_distr_r [in Coq.ZArith.Zmin]
Zplus_opp_expand [in Coq.ZArith.BinInt]
Zplus_opp_l [in Coq.ZArith.BinInt]
Zplus_opp_r [in Coq.ZArith.BinInt]
Zplus_permute [in Coq.ZArith.BinInt]
Zplus_reg_l [in Coq.ZArith.BinInt]
Zplus_succ_comm [in Coq.ZArith.BinInt]
Zplus_succ_l [in Coq.ZArith.BinInt]
Zplus_succ_r [in Coq.ZArith.BinInt]
Zplus_0_l [in Coq.ZArith.BinInt]
Zplus_0_r [in Coq.ZArith.BinInt]
Zplus_0_r_reverse [in Coq.ZArith.BinInt]
Zplus_0_simpl_l [in Coq.ZArith.BinInt]
Zplus_0_simpl_l_reverse [in Coq.ZArith.BinInt]
Zpos_eq_Z_of_nat_o_nat_of_P [in Coq.ZArith.Znat]
Zpos_mult_morphism [in Coq.ZArith.BinInt]
Zpos_plus_distr [in Coq.ZArith.BinInt]
Zpos_succ_morphism [in Coq.ZArith.BinInt]
Zpos_xI [in Coq.ZArith.BinInt]
Zpos_xO [in Coq.ZArith.BinInt]
Zpower_exp [in Coq.ZArith.Zpower]
Zpower_nat_is_exp [in Coq.ZArith.Zpower]
Zpower_nat_powerRZ [in Coq.Reals.Rfunctions]
Zpower_nat_powerRZ_absolu [in Coq.Reals.Rfunctions]
Zpower_NR0 [in Coq.Reals.Rfunctions]
Zpower_pos_is_exp [in Coq.ZArith.Zpower]
Zpower_pos_nat [in Coq.ZArith.Zpower]
Zpower_theory [in Coq.ZArith.Zpow_def]
Zpred'_succ' [in Coq.ZArith.BinInt]
Zpred_succ [in Coq.ZArith.BinInt]
Zred_factor0 [in Coq.ZArith.auxiliary]
Zred_factor1 [in Coq.ZArith.auxiliary]
Zred_factor2 [in Coq.ZArith.auxiliary]
Zred_factor3 [in Coq.ZArith.auxiliary]
Zred_factor4 [in Coq.ZArith.auxiliary]
Zred_factor5 [in Coq.ZArith.auxiliary]
Zred_factor6 [in Coq.ZArith.auxiliary]
Zsgn_Zabs [in Coq.ZArith.Zabs]
Zsplit2 [in Coq.ZArith.Zeven]
Zsqrt_interval [in Coq.ZArith.Zsqrt]
Zsucc'_discr [in Coq.ZArith.BinInt]
Zsucc_discr [in Coq.ZArith.BinInt]
Zsucc_eq_compat [in Coq.ZArith.BinInt]
Zsucc_gt_compat [in Coq.ZArith.Zorder]
Zsucc_gt_reg [in Coq.ZArith.Zorder]
Zsucc_inj [in Coq.ZArith.BinInt]
Zsucc_inj_contrapositive [in Coq.ZArith.BinInt]
Zsucc_le_compat [in Coq.ZArith.Zorder]
Zsucc_le_reg [in Coq.ZArith.Zorder]
Zsucc_lt_compat [in Coq.ZArith.Zorder]
Zsucc_lt_reg [in Coq.ZArith.Zorder]
Zsucc_max_distr [in Coq.ZArith.Zmax]
Zsucc_min_distr [in Coq.ZArith.Zmin]
Zsucc_pred [in Coq.ZArith.BinInt]
Ztrichotomy [in Coq.ZArith.Zorder]
Ztrichotomy_inf [in Coq.ZArith.Zorder]
Zwf_up_well_founded [in Coq.ZArith.Zwf]
Zwf_well_founded [in Coq.ZArith.Zwf]
Z2P_correct [in Coq.QArith.Qreduction]
Z2P_correct2 [in Coq.QArith.Qreduction]
Z_as_Int.i2z_eq [in Coq.ZArith.Int]
Z_as_Int.i2z_max [in Coq.ZArith.Int]
Z_as_Int.i2z_minus [in Coq.ZArith.Int]
Z_as_Int.i2z_mult [in Coq.ZArith.Int]
Z_as_Int.i2z_opp [in Coq.ZArith.Int]
Z_as_Int.i2z_plus [in Coq.ZArith.Int]
Z_as_Int.i2z_0 [in Coq.ZArith.Int]
Z_as_Int.i2z_1 [in Coq.ZArith.Int]
Z_as_Int.i2z_2 [in Coq.ZArith.Int]
Z_as_Int.i2z_3 [in Coq.ZArith.Int]
Z_dec [in Coq.ZArith.ZArith_dec]
Z_dec' [in Coq.ZArith.ZArith_dec]
Z_div2_value [in Coq.ZArith.Zbinary]
Z_div_exact_1 [in Coq.ZArith.Zdiv]
Z_div_exact_2 [in Coq.ZArith.Zdiv]
Z_div_ge [in Coq.ZArith.Zdiv]
Z_div_ge0 [in Coq.ZArith.Zdiv]
Z_div_lt [in Coq.ZArith.Zdiv]
Z_div_mod [in Coq.ZArith.Zdiv]
Z_div_mod_eq [in Coq.ZArith.Zdiv]
Z_div_mod_POS [in Coq.ZArith.Zdiv]
Z_div_mult [in Coq.ZArith.Zdiv]
Z_div_plus [in Coq.ZArith.Zdiv]
Z_div_POS_ge0 [in Coq.ZArith.Zdiv]
Z_div_same [in Coq.ZArith.Zdiv]
Z_eq_mult [in Coq.ZArith.BinInt]
Z_lt_abs_induction [in Coq.ZArith.Zcomplements]
Z_lt_abs_rec [in Coq.ZArith.Zcomplements]
Z_lt_induction [in Coq.ZArith.Wf_Z]
Z_lt_le_dec [in Coq.ZArith.ZArith_dec]
Z_lt_rec [in Coq.ZArith.Wf_Z]
Z_modulo_2 [in Coq.ZArith.Zeven]
Z_mod_lt [in Coq.ZArith.Zdiv]
Z_mod_plus [in Coq.ZArith.Zdiv]
Z_mod_same [in Coq.ZArith.Zdiv]
Z_mod_zero_opp [in Coq.ZArith.Zdiv]
Z_mult_div_ge [in Coq.ZArith.Zdiv]
Z_of_nat_complete [in Coq.ZArith.Wf_Z]
Z_of_nat_complete_inf [in Coq.ZArith.Wf_Z]
Z_of_nat_prop [in Coq.ZArith.Wf_Z]
Z_of_nat_set [in Coq.ZArith.Wf_Z]
Z_R_minus [in Coq.Reals.RIneq]
Z_to_binary [in Coq.ZArith.Zbinary]
Z_to_binary_Sn [in Coq.ZArith.Zbinary]
Z_to_binary_Sn_z [in Coq.ZArith.Zbinary]
Z_to_binary_to_Z [in Coq.ZArith.Zbinary]
Z_to_two_compl [in Coq.ZArith.Zbinary]
Z_to_two_compl_Sn [in Coq.ZArith.Zbinary]
Z_to_two_compl_Sn_z [in Coq.ZArith.Zbinary]
Z_to_two_compl_to_Z [in Coq.ZArith.Zbinary]

Global Index

(7984 entries)

Axiom Index

B

H

K

Q

V

W

X

Y

(401 entries)

Lemma Index

Y

(5228 entries)

Constructor Index

K

Q

W

Y

_

(292 entries)

Inductive Index

K

Y

_

(184 entries)

Definition Index

J

_

(1519 entries)

Module Index

A

B

C

G

H

J

L

Q

T

V

W

X

Y

_

(85 entries)

Library Index

K

V

X

Y

_

(275 entries)