| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (7984 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (401 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5228 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (292 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (184 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1519 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (85 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (275 entries) |
Z
Z [inductive, in Coq.ZArith.BinInt]Zabs [definition, in Coq.ZArith.BinInt]
Zabs [library]
Zabs_dec [definition, in Coq.ZArith.Zabs]
Zabs_eq [lemma, in Coq.ZArith.Zabs]
Zabs_eq_case [lemma, in Coq.ZArith.Zabs]
Zabs_ind [lemma, in Coq.ZArith.Zabs]
Zabs_intro [lemma, in Coq.ZArith.Zabs]
Zabs_N [definition, in Coq.ZArith.BinInt]
Zabs_nat [definition, in Coq.ZArith.BinInt]
Zabs_nat_lt [lemma, in Coq.ZArith.Zabs]
Zabs_non_eq [lemma, in Coq.ZArith.Zabs]
Zabs_pos [lemma, in Coq.ZArith.Zabs]
Zabs_triangle [lemma, in Coq.ZArith.Zabs]
Zabs_Zmult [lemma, in Coq.ZArith.Zabs]
Zabs_Zopp [lemma, in Coq.ZArith.Zabs]
Zabs_Zsgn [lemma, in Coq.ZArith.Zabs]
ZArith [library]
ZArith_base [library]
ZArith_dec [library]
Zbinary [library]
Zbool [library]
Zcase_sign [lemma, in Coq.ZArith.Zcomplements]
Zcompare [definition, in Coq.ZArith.BinInt]
Zcompare [library]
Zcompare_antisym [lemma, in Coq.ZArith.Zcompare]
Zcompare_egal_dec [lemma, in Coq.ZArith.Zcompare]
Zcompare_elim [lemma, in Coq.ZArith.Zcompare]
Zcompare_eq_case [lemma, in Coq.ZArith.Zcompare]
Zcompare_Eq_eq [lemma, in Coq.ZArith.Zcompare]
Zcompare_Eq_iff_eq [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_Lt_antisym [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_not_Lt [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_spec [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_trans [lemma, in Coq.ZArith.Zcompare]
Zcompare_mult_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_opp [lemma, in Coq.ZArith.Zcompare]
Zcompare_plus_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_rec [lemma, in Coq.ZArith.ZArith_dec]
Zcompare_refl [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_Gt [lemma, in Coq.ZArith.Zcompare]
Zcomplements [library]
ZC1 [lemma, in Coq.NArith.BinPos]
ZC2 [lemma, in Coq.NArith.BinPos]
ZC3 [lemma, in Coq.NArith.BinPos]
ZC4 [lemma, in Coq.NArith.BinPos]
Zdiv [definition, in Coq.ZArith.Zdiv]
Zdiv [library]
Zdivide [inductive, in Coq.ZArith.Znumtheory]
Zdivide_antisym [lemma, in Coq.ZArith.Znumtheory]
Zdivide_bounds [lemma, in Coq.ZArith.Znumtheory]
Zdivide_dec [lemma, in Coq.ZArith.Znumtheory]
Zdivide_factor_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_factor_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_intro [constructor, in Coq.ZArith.Znumtheory]
Zdivide_minus_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mod [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mult_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mult_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_l_rev [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r_rev [lemma, in Coq.ZArith.Znumtheory]
Zdivide_plus_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_refl [lemma, in Coq.ZArith.Znumtheory]
Zdivide_0 [lemma, in Coq.ZArith.Znumtheory]
Zdivide_1 [lemma, in Coq.ZArith.Znumtheory]
Zdiv2 [definition, in Coq.ZArith.Zeven]
Zdiv2_two_power_nat [lemma, in Coq.ZArith.Zbinary]
Zdiv_eucl [definition, in Coq.ZArith.Zdiv]
Zdiv_eucl_exist [lemma, in Coq.ZArith.Zdiv]
Zdiv_eucl_extended [lemma, in Coq.ZArith.Zdiv]
Zdiv_eucl_POS [definition, in Coq.ZArith.Zdiv]
Zdiv_rest [definition, in Coq.ZArith.Zpower]
Zdiv_rest_aux [definition, in Coq.ZArith.Zpower]
Zdiv_rest_correct [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_correct1 [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_correct2 [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_proof [constructor, in Coq.ZArith.Zpower]
Zdiv_rest_proofs [inductive, in Coq.ZArith.Zpower]
Zdouble [definition, in Coq.ZArith.BinInt]
Zdouble_minus_one [definition, in Coq.ZArith.BinInt]
Zdouble_plus_one [definition, in Coq.ZArith.BinInt]
Zegal_left [lemma, in Coq.ZArith.auxiliary]
Zeq_bool [definition, in Coq.ZArith.Zbool]
Zeq_le [lemma, in Coq.ZArith.Zorder]
Zeq_minus [lemma, in Coq.ZArith.BinInt]
Zeq_plus_swap [lemma, in Coq.ZArith.Zorder]
zero [definition, in Coq.Strings.Ascii]
zero [axiom, in Coq.Num.Params]
zero [axiom, in Coq.Num.Definitions]
zerob [definition, in Coq.Bool.Zerob]
Zerob [library]
zerob_false_elim [lemma, in Coq.Bool.Zerob]
zerob_false_intro [lemma, in Coq.Bool.Zerob]
zerob_true_elim [lemma, in Coq.Bool.Zerob]
zerob_true_intro [lemma, in Coq.Bool.Zerob]
zerop [definition, in Coq.Arith.Compare_dec]
zerop_bool [definition, in Coq.Arith.Bool_nat]
ZERO_le_N_digits [lemma, in Coq.ZArith.Zlogarithm]
Zeven [definition, in Coq.ZArith.Zeven]
Zeven [library]
Zeven_bit_value [lemma, in Coq.ZArith.Zbinary]
Zeven_bool [definition, in Coq.ZArith.Zeven]
Zeven_dec [definition, in Coq.ZArith.Zeven]
Zeven_div2 [lemma, in Coq.ZArith.Zeven]
Zeven_not_Zodd [lemma, in Coq.ZArith.Zeven]
Zeven_odd_bool [definition, in Coq.ZArith.Zbool]
Zeven_odd_dec [definition, in Coq.ZArith.Zeven]
Zeven_pred [lemma, in Coq.ZArith.Zeven]
Zeven_Sn [lemma, in Coq.ZArith.Zeven]
Zgcd [definition, in Coq.ZArith.Znumtheory]
Zgcd_is_gcd [lemma, in Coq.ZArith.Znumtheory]
Zgcd_is_pos [lemma, in Coq.ZArith.Znumtheory]
Zgcd_spec [lemma, in Coq.ZArith.Znumtheory]
Zge [definition, in Coq.ZArith.BinInt]
Zge_bool [definition, in Coq.ZArith.Zbool]
Zge_cases [lemma, in Coq.ZArith.Zbool]
Zge_compare [lemma, in Coq.ZArith.Zcompare]
Zge_iff_le [lemma, in Coq.ZArith.Zorder]
Zge_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zge_le [lemma, in Coq.ZArith.Zorder]
Zge_left [lemma, in Coq.ZArith.auxiliary]
Zge_minus_two_power_nat_S [lemma, in Coq.ZArith.Zbinary]
Zge_trans [lemma, in Coq.ZArith.Zorder]
Zge_trans_succ [lemma, in Coq.ZArith.Zorder]
Zggcd [definition, in Coq.ZArith.Znumtheory]
Zggcd_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Zggcd_gcd [lemma, in Coq.ZArith.Znumtheory]
Zgt [definition, in Coq.ZArith.BinInt]
Zgt_asym [lemma, in Coq.ZArith.Zorder]
Zgt_bool [definition, in Coq.ZArith.Zbool]
Zgt_cases [lemma, in Coq.ZArith.Zbool]
Zgt_compare [lemma, in Coq.ZArith.Zcompare]
Zgt_iff_lt [lemma, in Coq.ZArith.Zorder]
Zgt_irrefl [lemma, in Coq.ZArith.Zorder]
Zgt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zgt_left [lemma, in Coq.ZArith.auxiliary]
Zgt_left_gt [lemma, in Coq.ZArith.auxiliary]
Zgt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zgt_le_succ [lemma, in Coq.ZArith.Zorder]
Zgt_le_trans [lemma, in Coq.ZArith.Zorder]
Zgt_lt [lemma, in Coq.ZArith.Zorder]
Zgt_not_le [lemma, in Coq.ZArith.Zorder]
Zgt_pos_0 [lemma, in Coq.ZArith.Zorder]
Zgt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zgt_succ [lemma, in Coq.ZArith.Zorder]
Zgt_succ_gt_or_eq [lemma, in Coq.ZArith.Zorder]
Zgt_succ_le [lemma, in Coq.ZArith.Zorder]
Zgt_succ_pred [lemma, in Coq.ZArith.Zorder]
Zgt_trans [lemma, in Coq.ZArith.Zorder]
Zgt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zhints [library]
Zind [lemma, in Coq.ZArith.BinInt]
Zis_gcd [inductive, in Coq.ZArith.Znumtheory]
Zis_gcd_bezout [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_even_odd [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid2 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_intro [constructor, in Coq.ZArith.Znumtheory]
Zis_gcd_minus [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_mult [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_opp [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_refl [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_sym [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_uniqueness_apart_sign [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_0 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_0_abs [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_1 [lemma, in Coq.ZArith.Znumtheory]
Zle [definition, in Coq.ZArith.BinInt]
Zlength [definition, in Coq.ZArith.Zcomplements]
Zlength_aux [definition, in Coq.ZArith.Zcomplements]
Zlength_cons [lemma, in Coq.ZArith.Zcomplements]
Zlength_correct [lemma, in Coq.ZArith.Zcomplements]
Zlength_nil [lemma, in Coq.ZArith.Zcomplements]
Zlength_nil_inv [lemma, in Coq.ZArith.Zcomplements]
Zle_antisym [lemma, in Coq.ZArith.Zorder]
Zle_bool [definition, in Coq.ZArith.Zbool]
Zle_bool_antisym [lemma, in Coq.ZArith.Zbool]
Zle_bool_imp_le [lemma, in Coq.ZArith.Zbool]
Zle_bool_plus_mono [lemma, in Coq.ZArith.Zbool]
Zle_bool_refl [lemma, in Coq.ZArith.Zbool]
Zle_bool_total [definition, in Coq.ZArith.Zbool]
Zle_bool_trans [lemma, in Coq.ZArith.Zbool]
Zle_cases [lemma, in Coq.ZArith.Zbool]
Zle_compare [lemma, in Coq.ZArith.Zcompare]
Zle_ge [lemma, in Coq.ZArith.Zorder]
Zle_gt_trans [lemma, in Coq.ZArith.Zorder]
Zle_imp_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_left [lemma, in Coq.ZArith.auxiliary]
Zle_left_rev [lemma, in Coq.ZArith.auxiliary]
Zle_le_succ [lemma, in Coq.ZArith.Zorder]
Zle_lt_or_eq [lemma, in Coq.ZArith.Zorder]
Zle_lt_succ [lemma, in Coq.ZArith.Zorder]
Zle_lt_trans [lemma, in Coq.ZArith.Zorder]
Zle_max_l [lemma, in Coq.ZArith.Zmax]
Zle_max_r [lemma, in Coq.ZArith.Zmax]
Zle_minus_le_0 [lemma, in Coq.ZArith.Zorder]
Zle_min_l [lemma, in Coq.ZArith.Zmin]
Zle_min_r [lemma, in Coq.ZArith.Zmin]
Zle_mult_approx [lemma, in Coq.ZArith.auxiliary]
Zle_neg_pos [lemma, in Coq.ZArith.Zorder]
Zle_not_gt [lemma, in Coq.ZArith.Zorder]
Zle_not_lt [lemma, in Coq.ZArith.Zorder]
Zle_or_lt [lemma, in Coq.ZArith.Zorder]
Zle_plus_swap [lemma, in Coq.ZArith.Zorder]
Zle_pred [lemma, in Coq.ZArith.Zorder]
Zle_refl [lemma, in Coq.ZArith.Zorder]
Zle_succ [lemma, in Coq.ZArith.Zorder]
Zle_succ_le [lemma, in Coq.ZArith.Zorder]
Zle_trans [lemma, in Coq.ZArith.Zorder]
Zle_0_minus_le [lemma, in Coq.ZArith.Zorder]
Zle_0_nat [lemma, in Coq.ZArith.Zorder]
Zle_0_pos [lemma, in Coq.ZArith.Zorder]
Zle_0_1 [lemma, in Coq.ZArith.Zorder]
Zlogarithm [library]
Zlt [definition, in Coq.ZArith.BinInt]
Zlt_asym [lemma, in Coq.ZArith.Zorder]
Zlt_bool [definition, in Coq.ZArith.Zbool]
Zlt_cases [lemma, in Coq.ZArith.Zbool]
Zlt_compare [lemma, in Coq.ZArith.Zcompare]
Zlt_cotrans [lemma, in Coq.ZArith.ZArith_dec]
Zlt_cotrans_neg [lemma, in Coq.ZArith.ZArith_dec]
Zlt_cotrans_pos [lemma, in Coq.ZArith.ZArith_dec]
Zlt_gt [lemma, in Coq.ZArith.Zorder]
Zlt_gt_succ [lemma, in Coq.ZArith.Zorder]
Zlt_irrefl [lemma, in Coq.ZArith.Zorder]
Zlt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zlt_left [lemma, in Coq.ZArith.auxiliary]
Zlt_left_lt [lemma, in Coq.ZArith.auxiliary]
Zlt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zlt_le_succ [lemma, in Coq.ZArith.Zorder]
Zlt_le_trans [lemma, in Coq.ZArith.Zorder]
Zlt_le_weak [lemma, in Coq.ZArith.Zorder]
Zlt_lower_bound_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_lower_bound_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_lt_double [lemma, in Coq.ZArith.Zpower]
Zlt_lt_succ [lemma, in Coq.ZArith.Zorder]
Zlt_minus_simpl_swap [lemma, in Coq.ZArith.Zorder]
Zlt_neg_0 [lemma, in Coq.ZArith.Zorder]
Zlt_not_eq [lemma, in Coq.ZArith.Zorder]
Zlt_not_le [lemma, in Coq.ZArith.Zorder]
Zlt_plus_swap [lemma, in Coq.ZArith.Zorder]
Zlt_pred [lemma, in Coq.ZArith.Zorder]
Zlt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zlt_succ [lemma, in Coq.ZArith.Zorder]
Zlt_succ_gt [lemma, in Coq.ZArith.Zorder]
Zlt_succ_le [lemma, in Coq.ZArith.Zorder]
Zlt_succ_pred [lemma, in Coq.ZArith.Zorder]
Zlt_trans [lemma, in Coq.ZArith.Zorder]
Zlt_two_power_nat_S [lemma, in Coq.ZArith.Zbinary]
Zlt_0_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zlt_0_minus_lt [lemma, in Coq.ZArith.Zorder]
Zlt_0_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_0_1 [lemma, in Coq.ZArith.Zorder]
ZL0 [lemma, in Coq.ZArith.BinInt]
ZL10 [lemma, in Coq.NArith.BinPos]
ZL11 [lemma, in Coq.NArith.BinPos]
ZL16 [lemma, in Coq.NArith.Pnat]
ZL17 [lemma, in Coq.NArith.Pnat]
ZL3 [lemma, in Coq.NArith.Pnat]
ZL4 [lemma, in Coq.NArith.Pnat]
ZL4_inf [lemma, in Coq.ZArith.Wf_Z]
ZL5 [lemma, in Coq.NArith.Pnat]
ZL6 [lemma, in Coq.NArith.Pnat]
ZL7 [lemma, in Coq.NArith.Pnat]
ZL8 [lemma, in Coq.NArith.Pnat]
Zmax [definition, in Coq.ZArith.Zmax]
Zmax [library]
Zmax_assoc [lemma, in Coq.ZArith.Zmax]
Zmax_case [lemma, in Coq.ZArith.Zmax]
Zmax_case_strong [lemma, in Coq.ZArith.Zmax]
Zmax_comm [lemma, in Coq.ZArith.Zmax]
Zmax_idempotent [lemma, in Coq.ZArith.Zmax]
Zmax_irreducible_inf [lemma, in Coq.ZArith.Zmax]
Zmax_le_prime_inf [lemma, in Coq.ZArith.Zmax]
Zmax_lub [lemma, in Coq.ZArith.Zmax]
Zmax_min_absorption_r_r [lemma, in Coq.ZArith.Zminmax]
Zmax_min_distr_r [lemma, in Coq.ZArith.Zminmax]
Zmax_min_modular_r [lemma, in Coq.ZArith.Zminmax]
Zmin [definition, in Coq.ZArith.Zmin]
Zmin [library]
Zminmax [library]
Zminus [definition, in Coq.ZArith.BinInt]
Zminus_diag [lemma, in Coq.ZArith.BinInt]
Zminus_diag_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_eq [lemma, in Coq.ZArith.BinInt]
Zminus_plus [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_l [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_l_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_r [lemma, in Coq.ZArith.BinInt]
Zminus_succ_l [lemma, in Coq.ZArith.BinInt]
Zminus_0_l_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_0_r [lemma, in Coq.ZArith.BinInt]
Zmin_assoc [lemma, in Coq.ZArith.Zmin]
Zmin_case [lemma, in Coq.ZArith.Zmin]
Zmin_case_strong [lemma, in Coq.ZArith.Zmin]
Zmin_comm [lemma, in Coq.ZArith.Zmin]
Zmin_glb [lemma, in Coq.ZArith.Zmin]
Zmin_idempotent [lemma, in Coq.ZArith.Zmin]
Zmin_irreducible [lemma, in Coq.ZArith.Zmin]
Zmin_irreducible_inf [lemma, in Coq.ZArith.Zmin]
Zmin_le_prime_inf [lemma, in Coq.ZArith.Zmin]
Zmin_max_absorption_r_r [lemma, in Coq.ZArith.Zminmax]
Zmin_max_distr_r [lemma, in Coq.ZArith.Zminmax]
Zmin_max_modular_r [lemma, in Coq.ZArith.Zminmax]
Zmisc [library]
Zmod [definition, in Coq.ZArith.Zdiv]
Zmod2 [definition, in Coq.ZArith.Zbinary]
Zmod2_twice [lemma, in Coq.ZArith.Zbinary]
Zmod_divide [lemma, in Coq.ZArith.Znumtheory]
Zmult [definition, in Coq.ZArith.BinInt]
Zmult_assoc [lemma, in Coq.ZArith.BinInt]
Zmult_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_comm [lemma, in Coq.ZArith.BinInt]
Zmult_compare_compat_l [lemma, in Coq.ZArith.Zcompare]
Zmult_compare_compat_r [lemma, in Coq.ZArith.Zcompare]
Zmult_divide_compat_l [lemma, in Coq.ZArith.Znumtheory]
Zmult_divide_compat_r [lemma, in Coq.ZArith.Znumtheory]
Zmult_ge_compat [lemma, in Coq.ZArith.Zorder]
Zmult_ge_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_ge_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_ge_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_reg_l [lemma, in Coq.ZArith.Zorder]
Zmult_integral [lemma, in Coq.ZArith.BinInt]
Zmult_integral_l [lemma, in Coq.ZArith.BinInt]
Zmult_le_approx [lemma, in Coq.ZArith.auxiliary]
Zmult_le_compat [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_le_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_minus_distr_l [lemma, in Coq.ZArith.BinInt]
Zmult_minus_distr_r [lemma, in Coq.ZArith.BinInt]
Zmult_one [lemma, in Coq.ZArith.Znumtheory]
Zmult_opp_comm [lemma, in Coq.ZArith.BinInt]
Zmult_opp_opp [lemma, in Coq.ZArith.BinInt]
Zmult_permute [lemma, in Coq.ZArith.BinInt]
Zmult_plus_distr_l [lemma, in Coq.ZArith.BinInt]
Zmult_plus_distr_r [lemma, in Coq.ZArith.BinInt]
Zmult_reg_l [lemma, in Coq.ZArith.BinInt]
Zmult_reg_r [lemma, in Coq.ZArith.BinInt]
Zmult_succ_l [lemma, in Coq.ZArith.BinInt]
Zmult_succ_l_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_succ_r [lemma, in Coq.ZArith.BinInt]
Zmult_succ_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_0_l [lemma, in Coq.ZArith.BinInt]
Zmult_0_r [lemma, in Coq.ZArith.BinInt]
Zmult_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_1_inversion_l [lemma, in Coq.ZArith.BinInt]
Zmult_1_l [lemma, in Coq.ZArith.BinInt]
Zmult_1_r [lemma, in Coq.ZArith.BinInt]
Znat [library]
Zne [definition, in Coq.ZArith.BinInt]
Zneg [constructor, in Coq.ZArith.BinInt]
Zneg_plus_distr [lemma, in Coq.ZArith.BinInt]
Zneg_xI [lemma, in Coq.ZArith.BinInt]
Zneg_xO [lemma, in Coq.ZArith.BinInt]
Zneq_bool [definition, in Coq.ZArith.Zbool]
Zne_left [lemma, in Coq.ZArith.auxiliary]
Znot_ge_lt [lemma, in Coq.ZArith.Zorder]
Znot_gt_le [lemma, in Coq.ZArith.Zorder]
Znot_le_gt [lemma, in Coq.ZArith.Zorder]
Znot_le_succ [lemma, in Coq.ZArith.Zorder]
Znot_lt_ge [lemma, in Coq.ZArith.Zorder]
Znumtheory [library]
Zodd [definition, in Coq.ZArith.Zeven]
Zodd_bit_value [lemma, in Coq.ZArith.Zbinary]
Zodd_bool [definition, in Coq.ZArith.Zeven]
Zodd_dec [definition, in Coq.ZArith.Zeven]
Zodd_div2 [lemma, in Coq.ZArith.Zeven]
Zodd_div2_neg [lemma, in Coq.ZArith.Zeven]
Zodd_not_Zeven [lemma, in Coq.ZArith.Zeven]
Zodd_pred [lemma, in Coq.ZArith.Zeven]
Zodd_Sn [lemma, in Coq.ZArith.Zeven]
Zone_divide [lemma, in Coq.ZArith.Znumtheory]
Zone_min_pos [lemma, in Coq.ZArith.Zbool]
Zone_pos [lemma, in Coq.ZArith.Zbool]
Zopp [definition, in Coq.ZArith.BinInt]
Zopp_eq_mult_neg_1 [lemma, in Coq.ZArith.BinInt]
Zopp_inj [lemma, in Coq.ZArith.BinInt]
Zopp_involutive [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_l [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_l_reverse [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_r [lemma, in Coq.ZArith.BinInt]
Zopp_neg [lemma, in Coq.ZArith.BinInt]
Zopp_plus_distr [lemma, in Coq.ZArith.BinInt]
Zorder [library]
Zplus [definition, in Coq.ZArith.BinInt]
Zplus' [definition, in Coq.ZArith.BinInt]
Zplus_assoc [lemma, in Coq.ZArith.BinInt]
Zplus_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_comm [lemma, in Coq.ZArith.BinInt]
Zplus_compare_compat [lemma, in Coq.ZArith.Zcompare]
Zplus_diag_eq_mult_2 [lemma, in Coq.ZArith.BinInt]
Zplus_eq_compat [lemma, in Coq.ZArith.BinInt]
Zplus_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_gt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_compat [lemma, in Coq.ZArith.Zorder]
Zplus_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_lt_compat [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zplus_lt_compat [lemma, in Coq.ZArith.Zorder]
Zplus_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_lt_le_compat [lemma, in Coq.ZArith.Zorder]
Zplus_lt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_max_distr_r [lemma, in Coq.ZArith.Zmax]
Zplus_minus [lemma, in Coq.ZArith.BinInt]
Zplus_minus_eq [lemma, in Coq.ZArith.BinInt]
Zplus_min_distr_r [lemma, in Coq.ZArith.Zmin]
Zplus_opp_expand [lemma, in Coq.ZArith.BinInt]
Zplus_opp_l [lemma, in Coq.ZArith.BinInt]
Zplus_opp_r [lemma, in Coq.ZArith.BinInt]
Zplus_permute [lemma, in Coq.ZArith.BinInt]
Zplus_reg_l [lemma, in Coq.ZArith.BinInt]
Zplus_succ_comm [lemma, in Coq.ZArith.BinInt]
Zplus_succ_l [lemma, in Coq.ZArith.BinInt]
Zplus_succ_r [lemma, in Coq.ZArith.BinInt]
Zplus_0_l [lemma, in Coq.ZArith.BinInt]
Zplus_0_r [lemma, in Coq.ZArith.BinInt]
Zplus_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_0_simpl_l [lemma, in Coq.ZArith.BinInt]
Zplus_0_simpl_l_reverse [lemma, in Coq.ZArith.BinInt]
ZPminus [definition, in Coq.ZArith.BinInt]
Zpos [constructor, in Coq.ZArith.BinInt]
Zpos_eq_Z_of_nat_o_nat_of_P [lemma, in Coq.ZArith.Znat]
Zpos_mult_morphism [lemma, in Coq.ZArith.BinInt]
Zpos_plus_distr [lemma, in Coq.ZArith.BinInt]
Zpos_succ_morphism [lemma, in Coq.ZArith.BinInt]
Zpos_xI [lemma, in Coq.ZArith.BinInt]
Zpos_xO [lemma, in Coq.ZArith.BinInt]
Zpower [definition, in Coq.ZArith.Zpow_def]
Zpower [library]
Zpower_exp [lemma, in Coq.ZArith.Zpower]
Zpower_nat [definition, in Coq.ZArith.Zpower]
Zpower_nat_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_nat_powerRZ [lemma, in Coq.Reals.Rfunctions]
Zpower_nat_powerRZ_absolu [lemma, in Coq.Reals.Rfunctions]
Zpower_NR0 [lemma, in Coq.Reals.Rfunctions]
Zpower_pos [definition, in Coq.ZArith.Zpow_def]
Zpower_pos_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_pos_nat [lemma, in Coq.ZArith.Zpower]
Zpower_theory [lemma, in Coq.ZArith.Zpow_def]
Zpow_def [library]
Zpred [definition, in Coq.ZArith.BinInt]
Zpred' [definition, in Coq.ZArith.BinInt]
Zpred'_succ' [lemma, in Coq.ZArith.BinInt]
Zpred_succ [lemma, in Coq.ZArith.BinInt]
Zred_factor0 [lemma, in Coq.ZArith.auxiliary]
Zred_factor1 [lemma, in Coq.ZArith.auxiliary]
Zred_factor2 [lemma, in Coq.ZArith.auxiliary]
Zred_factor3 [lemma, in Coq.ZArith.auxiliary]
Zred_factor4 [lemma, in Coq.ZArith.auxiliary]
Zred_factor5 [lemma, in Coq.ZArith.auxiliary]
Zred_factor6 [lemma, in Coq.ZArith.auxiliary]
Zsgn [definition, in Coq.ZArith.BinInt]
Zsgn_Zabs [lemma, in Coq.ZArith.Zabs]
Zsplit2 [lemma, in Coq.ZArith.Zeven]
Zsqrt [definition, in Coq.ZArith.Zsqrt]
Zsqrt [library]
Zsqrt_interval [lemma, in Coq.ZArith.Zsqrt]
Zsqrt_plain [definition, in Coq.ZArith.Zsqrt]
Zsucc [definition, in Coq.ZArith.BinInt]
Zsucc' [definition, in Coq.ZArith.BinInt]
Zsucc'_discr [lemma, in Coq.ZArith.BinInt]
Zsucc_discr [lemma, in Coq.ZArith.BinInt]
Zsucc_eq_compat [lemma, in Coq.ZArith.BinInt]
Zsucc_gt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_gt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_inj [lemma, in Coq.ZArith.BinInt]
Zsucc_inj_contrapositive [lemma, in Coq.ZArith.BinInt]
Zsucc_le_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_le_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_lt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_lt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_max_distr [lemma, in Coq.ZArith.Zmax]
Zsucc_min_distr [lemma, in Coq.ZArith.Zmin]
Zsucc_pred [lemma, in Coq.ZArith.BinInt]
Ztrichotomy [lemma, in Coq.ZArith.Zorder]
Ztrichotomy_inf [lemma, in Coq.ZArith.Zorder]
Zwf [definition, in Coq.ZArith.Zwf]
Zwf [library]
Zwf_up [definition, in Coq.ZArith.Zwf]
Zwf_up_well_founded [lemma, in Coq.ZArith.Zwf]
Zwf_well_founded [lemma, in Coq.ZArith.Zwf]
Z0 [constructor, in Coq.ZArith.BinInt]
Z2P [definition, in Coq.QArith.Qreduction]
Z2P_correct [lemma, in Coq.QArith.Qreduction]
Z2P_correct2 [lemma, in Coq.QArith.Qreduction]
Z_as_DT [module, in Coq.Logic.DecidableTypeEx]
Z_as_Int [module, in Coq.ZArith.Int]
Z_as_Int.eq_dec [definition, in Coq.ZArith.Int]
Z_as_Int.ge_lt_dec [definition, in Coq.ZArith.Int]
Z_as_Int.gt_le_dec [definition, in Coq.ZArith.Int]
Z_as_Int.int [definition, in Coq.ZArith.Int]
Z_as_Int.i2z [definition, in Coq.ZArith.Int]
Z_as_Int.i2z_eq [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_max [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_minus [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_mult [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_opp [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_plus [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_0 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_1 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_2 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_3 [lemma, in Coq.ZArith.Int]
Z_as_Int.max [definition, in Coq.ZArith.Int]
Z_as_Int.minus [definition, in Coq.ZArith.Int]
Z_as_Int.mult [definition, in Coq.ZArith.Int]
Z_as_Int.opp [definition, in Coq.ZArith.Int]
Z_as_Int.plus [definition, in Coq.ZArith.Int]
Z_as_Int._0 [definition, in Coq.ZArith.Int]
Z_as_Int._1 [definition, in Coq.ZArith.Int]
Z_as_Int._2 [definition, in Coq.ZArith.Int]
Z_as_Int._3 [definition, in Coq.ZArith.Int]
Z_as_OT [module, in Coq.FSets.OrderedTypeEx]
Z_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_dec' [lemma, in Coq.ZArith.ZArith_dec]
Z_div2_value [lemma, in Coq.ZArith.Zbinary]
Z_div_exact_1 [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_2 [lemma, in Coq.ZArith.Zdiv]
Z_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_div_ge0 [lemma, in Coq.ZArith.Zdiv]
Z_div_lt [lemma, in Coq.ZArith.Zdiv]
Z_div_mod [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_eq [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_POS [lemma, in Coq.ZArith.Zdiv]
Z_div_mult [lemma, in Coq.ZArith.Zdiv]
Z_div_plus [lemma, in Coq.ZArith.Zdiv]
Z_div_POS_ge0 [lemma, in Coq.ZArith.Zdiv]
Z_div_same [lemma, in Coq.ZArith.Zdiv]
Z_eq_bool [definition, in Coq.ZArith.Zbool]
Z_eq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_eq_mult [lemma, in Coq.ZArith.BinInt]
Z_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_ge_lt_bool [definition, in Coq.ZArith.Zbool]
Z_ge_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_gt_le_bool [definition, in Coq.ZArith.Zbool]
Z_gt_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_le_gt_bool [definition, in Coq.ZArith.Zbool]
Z_le_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_le_lt_eq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_lt_abs_induction [lemma, in Coq.ZArith.Zcomplements]
Z_lt_abs_rec [lemma, in Coq.ZArith.Zcomplements]
Z_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_lt_ge_bool [definition, in Coq.ZArith.Zbool]
Z_lt_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_lt_induction [lemma, in Coq.ZArith.Wf_Z]
Z_lt_le_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_lt_rec [lemma, in Coq.ZArith.Wf_Z]
Z_modulo_2 [lemma, in Coq.ZArith.Zeven]
Z_mod_lt [lemma, in Coq.ZArith.Zdiv]
Z_mod_plus [lemma, in Coq.ZArith.Zdiv]
Z_mod_same [lemma, in Coq.ZArith.Zdiv]
Z_mod_zero_opp [lemma, in Coq.ZArith.Zdiv]
Z_mult_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_noteq_bool [definition, in Coq.ZArith.Zbool]
Z_noteq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_notzerop [definition, in Coq.ZArith.ZArith_dec]
Z_of_N [definition, in Coq.ZArith.BinInt]
Z_of_nat [definition, in Coq.ZArith.BinInt]
Z_of_nat_complete [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_complete_inf [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_prop [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_set [lemma, in Coq.ZArith.Wf_Z]
Z_R_minus [lemma, in Coq.Reals.RIneq]
Z_to_binary [lemma, in Coq.ZArith.Zbinary]
Z_to_binary_Sn [lemma, in Coq.ZArith.Zbinary]
Z_to_binary_Sn_z [lemma, in Coq.ZArith.Zbinary]
Z_to_binary_to_Z [lemma, in Coq.ZArith.Zbinary]
Z_to_two_compl [lemma, in Coq.ZArith.Zbinary]
Z_to_two_compl_Sn [lemma, in Coq.ZArith.Zbinary]
Z_to_two_compl_Sn_z [lemma, in Coq.ZArith.Zbinary]
Z_to_two_compl_to_Z [lemma, in Coq.ZArith.Zbinary]
Z_zerop [definition, in Coq.ZArith.ZArith_dec]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (7984 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (401 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5228 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (292 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (184 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (1519 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (85 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (275 entries) |