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