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 (25958 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 (999 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 (811 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 (1769 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 (587 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 (11879 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 (960 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 (508 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 (307 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 (479 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 (495 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 (905 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 (1199 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 (4894 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 (166 entries)

Z

Z [module, in Coq.ZArith.BinIntDef]
Z [abbreviation, in Coq.ZArith.BinInt]
Z [module, in Coq.ZArith.BinInt]
Z [module, in Coq.Floats.FloatOps]
Z [inductive, in Coq.Numbers.BinNums]
Z [module, in Coq.omega.PreOmega]
Z [module, in Coq.Numbers.Integer.Binary.ZBinary]
Z [module, in Coq.ZArith.Zbitwise]
Zabs [library]
ZabsSpec [instance, in Coq.micromega.ZifyInst]
Zabs_nat_lt [lemma, in Coq.ZArith.Zabs]
Zabs_nat_le [lemma, in Coq.ZArith.Zabs]
Zabs_nat_compare [abbreviation, in Coq.ZArith.Zabs]
Zabs_nat_Zminus [abbreviation, in Coq.ZArith.Zabs]
Zabs_nat_Zplus [abbreviation, in Coq.ZArith.Zabs]
Zabs_nat_Zsucc [abbreviation, in Coq.ZArith.Zabs]
Zabs_nat_mult [abbreviation, in Coq.ZArith.Zabs]
Zabs_nat_Z_of_nat [abbreviation, in Coq.ZArith.Zabs]
Zabs_spec [lemma, in Coq.ZArith.Zabs]
Zabs_dec [definition, in Coq.ZArith.Zabs]
Zabs_intro [lemma, in Coq.ZArith.Zabs]
Zabs_ind [lemma, in Coq.ZArith.Zabs]
Zabs_Zmult [abbreviation, in Coq.ZArith.Zabs]
Zabs_Zsgn [abbreviation, in Coq.ZArith.Zabs]
Zabs_eq_case [abbreviation, in Coq.ZArith.Zabs]
Zabs_pos [abbreviation, in Coq.ZArith.Zabs]
Zabs_Zopp [abbreviation, in Coq.ZArith.Zabs]
Zabs_non_eq [abbreviation, in Coq.ZArith.Zabs]
Zabs_Qabs [lemma, in Coq.QArith.Qabs]
Zabs_N_mult [abbreviation, in Coq.ZArith.Znat]
Zabs_N_mult_abs [abbreviation, in Coq.ZArith.Znat]
Zabs_N_plus [abbreviation, in Coq.ZArith.Znat]
Zabs_N_plus_abs [abbreviation, in Coq.ZArith.Znat]
Zabs_N_succ [abbreviation, in Coq.ZArith.Znat]
Zabs_N_succ_abs [abbreviation, in Coq.ZArith.Znat]
Zabs_of_N [abbreviation, in Coq.ZArith.Znat]
Zabs_nat_N [lemma, in Coq.ZArith.Znat]
Zabs_N_nat [lemma, in Coq.ZArith.Znat]
Zabs_non_eq [abbreviation, in Coq.ZArith.Zcompare]
Zabs2N [module, in Coq.ZArith.Znat]
Zabs2Nat [module, in Coq.ZArith.Znat]
Zabs2Nat.abs_nat_nonneg [lemma, in Coq.ZArith.Znat]
Zabs2Nat.abs_nat_spec [lemma, in Coq.ZArith.Znat]
Zabs2Nat.id [lemma, in Coq.ZArith.Znat]
Zabs2Nat.id_abs [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_mul_abs [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_add_abs [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_succ_abs [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_max [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_min [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_lt [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_le [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_compare [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_pred [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_sub [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_mul [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_add [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_succ [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_neg [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_pos [lemma, in Coq.ZArith.Znat]
Zabs2Nat.inj_0 [lemma, in Coq.ZArith.Znat]
Zabs2N.abs_N_nonneg [lemma, in Coq.ZArith.Znat]
Zabs2N.abs_N_spec [lemma, in Coq.ZArith.Znat]
Zabs2N.id [lemma, in Coq.ZArith.Znat]
Zabs2N.id_abs [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_mul_abs [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_add_abs [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_succ_abs [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_pow [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_rem [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_quot [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_max [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_min [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_lt [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_le [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_compare [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_pred [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_sub [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_mul [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_add [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_succ [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_opp [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_neg [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_pos [lemma, in Coq.ZArith.Znat]
Zabs2N.inj_0 [lemma, in Coq.ZArith.Znat]
ZAdd [library]
ZAddOrder [library]
ZAddOrderProp [module, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.add_nonpos_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.add_nonpos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.add_neg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.add_neg_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_sub_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_sub_le_add [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_sub_le_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_sub_le_add_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_add_le_sub_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_add_le_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_le_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_lt_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_sub_0 [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.le_0_sub [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_sub_pos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_sub_lt_add [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_sub_lt_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_sub_lt_add_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_add_lt_sub_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_add_lt_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_le_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_m1_0 [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_sub_0 [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.lt_0_sub [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_nonpos_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_nonneg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_neg_pos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_pos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.opp_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.PosNeg [section, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.PosNeg.P [variable, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.PosNeg.P_wd [variable, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_nonpos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_neg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_le_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_lt_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_le_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_lt_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_le_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_le_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_lt_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_lt_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_nonpos [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_neg [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_nonneg [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.sub_pos [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderProp.zero_pos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddProp [module, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_add_simpl_r_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_add_simpl_r_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_add_simpl_l_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_add_simpl_l_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_simpl_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_simpl_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_move_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_move_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_move_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_move_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_sub_swap [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_sub_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_opp_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_opp_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.add_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.eq_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.eq_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_inj_wd [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_inj [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_sub_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_add_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_involutive [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.opp_pred [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_add_simpl_r_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_add_simpl_r_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_add [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_simpl_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_simpl_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_move_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_move_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_move_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_move_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_sub_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_add_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_diag [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_succ_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddProp.sub_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZArith [library]
ZArithProof [inductive, in Coq.micromega.ZMicromega]
ZArithProof_sind [definition, in Coq.micromega.ZMicromega]
ZArithProof_rec [definition, in Coq.micromega.ZMicromega]
ZArithProof_ind [definition, in Coq.micromega.ZMicromega]
ZArithProof_rect [definition, in Coq.micromega.ZMicromega]
ZArithRing [library]
ZArith_base [library]
ZArith_dec [library]
ZArith_hints [library]
ZAxiom [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxioms [library]
ZAxiomsMiniSig [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxiomsMiniSig' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxiomsSig [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxiomsSig' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxiom.succ_pred [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZBase [library]
ZBaseProp [module, in Coq.Numbers.Integer.Abstract.ZBase]
ZBaseProp.pred_inj_wd [lemma, in Coq.Numbers.Integer.Abstract.ZBase]
ZBaseProp.pred_inj [lemma, in Coq.Numbers.Integer.Abstract.ZBase]
ZBaseProp.succ_m1 [lemma, in Coq.Numbers.Integer.Abstract.ZBase]
ZBasicProp [module, in Coq.Numbers.Integer.Abstract.ZProperties]
ZBinary [library]
ZBits [library]
ZBitsProp [module, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_nocarry_mod_lt_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_nocarry_lt_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_nocarry_lxor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_bit1 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_carry_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_carry_bits_aux [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_carry_div2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_bit0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_lnot_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_b2z_double_bit0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add_b2z_double_div2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add3_bits_div2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.add3_bit0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.are_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_inj_iff' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_inj' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_inj_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_inj [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_inj_0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_neg_ex [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_neg' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_nonneg_ex [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_nonneg' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_iff_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_above_log2_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_above_log2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_m1 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_opp [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bits_0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bit_log2_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bit_log2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bit0_mod [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bit0_eqb [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.bit0_odd [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.b2z [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.b2z_bit0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.b2z_div2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.b2z_inj [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.b2z_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_neq [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_eq [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_eqb [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.clearbit_spec' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div_pow2_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_odd [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_div [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.div2_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.double_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.double_bits_succ [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.eqf [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.eqf_equiv [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.exists_div2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_ones_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_ones [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_lnot_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_m1_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_m1_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_ldiff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_lor_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_lor_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_comm [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.land_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_le [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_ones_l_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_ones_r_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_ones_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_land [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_m1_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_m1_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_ldiff_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ldiff_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnextcarry [abbreviation, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_shiftr [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_lxor_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_lxor_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_ldiff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_land [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_lor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_m1 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_involutive [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_spec [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lnot_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_lxor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_land [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_lor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_shiftl' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_shiftl [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_shiftr [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.log2_bits_unique [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_ones_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_lnot_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_m1_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_m1_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_ldiff_and [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_land_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_land_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_eq_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_eq_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_diag [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_comm [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lor_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_lor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_m1_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_m1_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_lnot_lnot [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_comm [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_eq_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_nilpotent [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_eq [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.lxor3 [abbreviation, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.mod_pow2_bits_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.mod_pow2_bits_high [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.mul_pow2_bits_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.mul_pow2_bits [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.mul_pow2_bits_add [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.nextcarry [abbreviation, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.nocarry_equiv [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_spec_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_spec_high [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_spec_low [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_mod_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_div_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_add [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_equiv [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.ones_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.pow_div_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.pow_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.pow2_bits_eqb [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.pow2_bits_false [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.pow2_bits_true [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit [definition, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_neq [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_eq [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_eqb [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.setbit_spec' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_ldiff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_lor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_land [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_lxor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_eq_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_shiftl [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_spec_alt [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_div_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_mul_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftl_spec [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_neg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_ldiff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_lor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_land [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_lxor [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_eq_0 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_eq_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_shiftr [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_shiftl_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_shiftl_l [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_wd [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_mul_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_div_pow2 [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.shiftr_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.sub_nocarry_ldiff [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_eqf [instance, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_odd [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_unique [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_eqb [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_false [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_true [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_spec [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_spec' [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_succ_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.testbit_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZBits]
ZBitsProp.xor3 [abbreviation, in Coq.Numbers.Integer.Abstract.ZBits]
_ === _ [notation, in Coq.Numbers.Integer.Abstract.ZBits]
Zbitwise [library]
Zbool [library]
Zcase_sign [lemma, in Coq.ZArith.Zcomplements]
ZChecker [definition, in Coq.micromega.ZMicromega]
ZChecker_sound [lemma, in Coq.micromega.ZMicromega]
Zcleb_morph [lemma, in Coq.micromega.ZCoeff]
Zcneqb_morph [lemma, in Coq.micromega.ZCoeff]
ZCoeff [library]
Zcompare [library]
ZcompareSpec [instance, in Coq.micromega.ZifyComparison]
ZcompareZ [definition, in Coq.micromega.ZifyComparison]
Zcompare_rec [lemma, in Coq.ZArith.ZArith_dec]
Zcompare_rect [lemma, in Coq.ZArith.ZArith_dec]
Zcompare_spec [lemma, in Coq.micromega.ZifyComparison]
Zcompare_Eq_iff_eq [abbreviation, in Coq.ZArith.Zcompare]
Zcompare_Eq_eq [abbreviation, in Coq.ZArith.Zcompare]
Zcompare_eq_case [lemma, in Coq.ZArith.Zcompare]
Zcompare_elim [lemma, in Coq.ZArith.Zcompare]
Zcompare_mult_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_not_Lt [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_Gt [lemma, in Coq.ZArith.Zcompare]
Zcompare_plus_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_spec [lemma, in Coq.ZArith.Zcompare]
Zcompare_opp [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_trans [lemma, in Coq.ZArith.Zcompare]
Zcompare_Lt_trans [lemma, in Coq.ZArith.Zcompare]
Zcompare_antisym [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_Lt_antisym [lemma, in Coq.ZArith.Zcompare]
Zcomplements [library]
Zcri [instance, in Coq.nsatz.NsatzTactic]
Zcri [instance, in Coq.setoid_ring.Cring]
Zcri [instance, in Coq.setoid_ring.Rings_Z]
ZC1 [abbreviation, in Coq.PArith.BinPos]
ZC2 [abbreviation, in Coq.PArith.BinPos]
ZC4 [lemma, in Coq.PArith.BinPos]
ZDecAxiomsSig [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZDecAxiomsSig' [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
Zdeduce [definition, in Coq.micromega.ZMicromega]
Zdi [instance, in Coq.nsatz.NsatzTactic]
Zdi [instance, in Coq.setoid_ring.Rings_Z]
Zdigits2 [definition, in Coq.Floats.SpecFloat]
ZDiv [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Zdiv [library]
ZDivEucl [library]
ZDivFloor [library]
Zdivide_power_2 [lemma, in Coq.ZArith.Zpow_facts]
Zdivide_Zgcd [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mod_minus [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zdiv_lt_pos [lemma, in Coq.ZArith.Znumtheory]
Zdivide_le [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zdiv_eq_2 [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zdiv_eq [lemma, in Coq.ZArith.Znumtheory]
Zdivide_dec [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mod [lemma, in Coq.ZArith.Znumtheory]
Zdivide_bounds [lemma, in Coq.ZArith.Znumtheory]
Zdivide_1 [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_Zabs_inv_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zabs_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_l_rev [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r_rev [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_factor_l [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_factor_r [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_mult_r [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_mult_l [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_minus_l [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_plus_r [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_0 [abbreviation, in Coq.ZArith.Znumtheory]
Zdivide_intro [definition, in Coq.ZArith.Znumtheory]
Zdivide_pol_sub_0 [lemma, in Coq.micromega.ZMicromega]
Zdivide_pol_sub [lemma, in Coq.micromega.ZMicromega]
Zdivide_pol_one [lemma, in Coq.micromega.ZMicromega]
Zdivide_pol_Zdivide [lemma, in Coq.micromega.ZMicromega]
Zdivide_pol_sind [definition, in Coq.micromega.ZMicromega]
Zdivide_pol_ind [definition, in Coq.micromega.ZMicromega]
Zdivide_pol [inductive, in Coq.micromega.ZMicromega]
Zdivide_ceiling [lemma, in Coq.micromega.ZMicromega]
ZDivProp [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.add_mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.add_mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.add_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.add_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.add_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_unique_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_opp_r_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_opp_r_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_unique_neg [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_unique_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.div_mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_sign_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_sign [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_sign_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_opp_r_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_opp_r_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_bound_or [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_unique_neg [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_unique_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_bound_abs [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mod_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_succ_div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_succ_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_div_ge [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.mul_div_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.opp_mod_bound_or [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.Private_NZDiv [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivProp.rem_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSpecific [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZDivSpecific.mod_neg_bound [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZDivSpecific.mod_pos_bound [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZDivTrunc [library]
Zdiv_eucl_extended [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_le [lemma, in Coq.ZArith.Zdiv]
Zdiv_Zdiv [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_cancel_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_cancel_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_opp_opp [lemma, in Coq.ZArith.Zdiv]
Zdiv_sgn [lemma, in Coq.ZArith.Zdiv]
Zdiv_le_compat_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_le_lower_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_le_upper_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_lt_upper_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_small [lemma, in Coq.ZArith.Zdiv]
Zdiv_1_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_1_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_0_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_0_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_unique [lemma, in Coq.ZArith.Zdiv]
Zdiv_unique_full [lemma, in Coq.ZArith.Zdiv]
Zdiv_mod_unique_2 [lemma, in Coq.ZArith.Zdiv]
Zdiv_mod_unique [lemma, in Coq.ZArith.Zdiv]
Zdiv_eucl_exist [lemma, in Coq.ZArith.Zdiv]
Zdiv_eucl_POS [abbreviation, in Coq.ZArith.Zdiv]
Zdiv_rest_shiftr [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_ok [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_correct [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_proofs_sind [definition, in Coq.ZArith.Zpower]
Zdiv_rest_proofs_rec [definition, in Coq.ZArith.Zpower]
Zdiv_rest_proofs_ind [definition, in Coq.ZArith.Zpower]
Zdiv_rest_proofs_rect [definition, in Coq.ZArith.Zpower]
Zdiv_rest_proof [constructor, in Coq.ZArith.Zpower]
Zdiv_rest_proofs [inductive, in Coq.ZArith.Zpower]
Zdiv_rest_correct2 [lemma, in Coq.ZArith.Zpower]
Zdiv_rest_correct1 [lemma, in Coq.ZArith.Zpower]
Zdiv_rest [definition, in Coq.ZArith.Zpower]
Zdiv_rest_aux [definition, in Coq.ZArith.Zpower]
Zdiv_Qdiv [lemma, in Coq.QArith.Qround]
Zdiv_pol_correct [lemma, in Coq.micromega.ZMicromega]
Zdiv_PX [constructor, in Coq.micromega.ZMicromega]
Zdiv_Pinj [constructor, in Coq.micromega.ZMicromega]
Zdiv_Pc [constructor, in Coq.micromega.ZMicromega]
Zdiv_pol [definition, in Coq.micromega.ZMicromega]
ZDiv' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Zdiv2_odd_eqn [lemma, in Coq.ZArith.Zeven]
Zdiv2_div [lemma, in Coq.ZArith.Zdiv]
Zdouble_plus_one_mult [abbreviation, in Coq.ZArith.BinInt]
Zdouble_mult [abbreviation, in Coq.ZArith.BinInt]
Zdouble_minus_one [abbreviation, in Coq.ZArith.BinInt]
Zdouble_plus_one [abbreviation, in Coq.ZArith.BinInt]
Zegal_left [lemma, in Coq.ZArith.auxiliary]
Zeqb_ok [lemma, in Coq.setoid_ring.Ncring_tac]
Zeqe [lemma, in Coq.setoid_ring.InitialRing]
Zeq_bool_complete [lemma, in Coq.setoid_ring.RealField]
Zeq_minus [lemma, in Coq.ZArith.BinInt]
Zeq_plus_swap [lemma, in Coq.ZArith.Zorder]
Zeq_le [abbreviation, in Coq.ZArith.Zorder]
Zeq_bool_if [lemma, in Coq.ZArith.Zbool]
Zeq_bool_neq [lemma, in Coq.ZArith.Zbool]
Zeq_bool_eq [lemma, in Coq.ZArith.Zbool]
Zeq_is_eq_bool [lemma, in Coq.ZArith.Zbool]
Zeq_bool [definition, in Coq.ZArith.Zbool]
Zeq_bool_IZR [lemma, in Coq.Reals.RIneq]
zero [abbreviation, in Coq.Init.Decimal]
zero [definition, in Coq.Floats.PrimFloat]
zero [definition, in Coq.Init.Nat]
zero [projection, in Coq.setoid_ring.Algebra_syntax]
Zero [record, in Coq.setoid_ring.Algebra_syntax]
zero [constructor, in Coq.setoid_ring.Algebra_syntax]
Zero [inductive, in Coq.setoid_ring.Algebra_syntax]
zero [abbreviation, in Coq.Init.Hexadecimal]
zero [definition, in Coq.Strings.Ascii]
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]
ZeroSuccPred [module, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPredNotation [module, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPredNotation.P [abbreviation, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPredNotation.S [abbreviation, in Coq.Numbers.NatInt.NZAxioms]
0 [notation, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPred' [module, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPred.pred [axiom, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPred.succ [axiom, in Coq.Numbers.NatInt.NZAxioms]
ZeroSuccPred.zero [axiom, in Coq.Numbers.NatInt.NZAxioms]
zero_notation [instance, in Coq.setoid_ring.Ncring]
ZEuclid [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclid [module, in Coq.ZArith.Zeuclid]
Zeuclid [library]
ZEuclidProp [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.add_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.add_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.add_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_unique_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_opp_opp_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_opp_opp_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.div_mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_divides [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_opp_opp_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_opp_opp_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mod_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_pred_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_succ_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.mul_div_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclidProp.Private_NZDiv [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
_ mod _ (euclid) [notation, in Coq.Numbers.Integer.Abstract.ZDivEucl]
_ / _ (euclid) [notation, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZEuclid.div [definition, in Coq.ZArith.Zeuclid]
ZEuclid.div_mod [lemma, in Coq.ZArith.Zeuclid]
ZEuclid.div_wd [instance, in Coq.ZArith.Zeuclid]
ZEuclid.modulo [definition, in Coq.ZArith.Zeuclid]
ZEuclid.mod_bound_pos [lemma, in Coq.ZArith.Zeuclid]
ZEuclid.mod_always_pos [lemma, in Coq.ZArith.Zeuclid]
ZEuclid.mod_wd [instance, in Coq.ZArith.Zeuclid]
Zeval_nformula_dec [lemma, in Coq.micromega.ZMicromega]
Zeval_op1 [definition, in Coq.micromega.ZMicromega]
Zeval_formula_compat' [lemma, in Coq.micromega.ZMicromega]
Zeval_formula_compat [lemma, in Coq.micromega.ZMicromega]
Zeval_formula' [definition, in Coq.micromega.ZMicromega]
Zeval_formula [definition, in Coq.micromega.ZMicromega]
Zeval_op2_hold [lemma, in Coq.micromega.ZMicromega]
Zeval_op2 [definition, in Coq.micromega.ZMicromega]
Zeval_bop2 [definition, in Coq.micromega.ZMicromega]
Zeval_pop2 [definition, in Coq.micromega.ZMicromega]
Zeval_expr_compat [lemma, in Coq.micromega.ZMicromega]
Zeval_const [definition, in Coq.micromega.ZMicromega]
Zeval_expr [definition, in Coq.micromega.ZMicromega]
Zeven [definition, in Coq.ZArith.Zeven]
Zeven [library]
Zeven_mult_Zeven_r [lemma, in Coq.ZArith.Zeven]
Zeven_mult_Zeven_l [lemma, in Coq.ZArith.Zeven]
Zeven_plus_Zeven [lemma, in Coq.ZArith.Zeven]
Zeven_plus_Zodd [lemma, in Coq.ZArith.Zeven]
Zeven_2p [lemma, in Coq.ZArith.Zeven]
Zeven_ex [lemma, in Coq.ZArith.Zeven]
Zeven_quot2 [lemma, in Coq.ZArith.Zeven]
Zeven_div2 [lemma, in Coq.ZArith.Zeven]
Zeven_bool_pred [abbreviation, in Coq.ZArith.Zeven]
Zeven_bool_succ [abbreviation, in Coq.ZArith.Zeven]
Zeven_pred [lemma, in Coq.ZArith.Zeven]
Zeven_Sn [lemma, in Coq.ZArith.Zeven]
Zeven_not_Zodd [lemma, in Coq.ZArith.Zeven]
Zeven_dec [definition, in Coq.ZArith.Zeven]
Zeven_odd_dec [definition, in Coq.ZArith.Zeven]
Zeven_odd_bool [lemma, in Coq.ZArith.Zeven]
Zeven_bool_iff [lemma, in Coq.ZArith.Zeven]
Zeven_bool [abbreviation, in Coq.ZArith.Zeven]
Zeven_ex_iff [lemma, in Coq.ZArith.Zeven]
Zeven_equiv [lemma, in Coq.ZArith.Zeven]
Zeven_mod [lemma, in Coq.ZArith.Zdiv]
Zeven_odd_bool [definition, in Coq.ZArith.Zbool]
Zeven_rem [lemma, in Coq.ZArith.Zquot]
ZExtraProp [module, in Coq.Numbers.Integer.Abstract.ZProperties]
ZGcd [library]
ZgcdM [definition, in Coq.micromega.ZMicromega]
Zgcdn [definition, in Coq.ZArith.Zgcd_alt]
Zgcdn_is_gcd [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_is_gcd_pos [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_opp [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_ok_before_fibonacci [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_worst_is_fibonacci [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_linear_bound [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_pos [lemma, in Coq.ZArith.Zgcd_alt]
ZGcdProp [module, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.Bezout [definition, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.bezout_1_gcd [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.Bezout_wd [instance, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_mul_split [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_add_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_antisym [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_antisym_abs [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_1_r_abs [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_abs_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_abs_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.divide_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gauss [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_mul_mono_r_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_mul_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_mul_mono_l_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_mul_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_bezout [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_sub_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_add_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_add_mult_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_diag [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_abs_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_abs_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
ZGcdProp.gcd_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZGcd]
Zgcd_is_gcd [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_bound_opp [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_bound_fibonacci [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_alt_pos [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_alt [definition, in Coq.ZArith.Zgcd_alt]
Zgcd_bound [definition, in Coq.ZArith.Zgcd_alt]
Zgcd_1_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Zgcd_1 [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_0 [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_Zabs [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_ass [lemma, in Coq.ZArith.Znumtheory]
Zgcd_div_swap [lemma, in Coq.ZArith.Znumtheory]
Zgcd_div_swap0 [lemma, in Coq.ZArith.Znumtheory]
Zgcd_inv_0_r [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_inv_0_l [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_spec [lemma, in Coq.ZArith.Znumtheory]
Zgcd_is_pos [abbreviation, in Coq.ZArith.Znumtheory]
Zgcd_is_gcd [lemma, in Coq.ZArith.Znumtheory]
Zgcd_pol_correct_lt [lemma, in Coq.micromega.ZMicromega]
Zgcd_pol_div [lemma, in Coq.micromega.ZMicromega]
Zgcd_minus [lemma, in Coq.micromega.ZMicromega]
Zgcd_pol_ge [lemma, in Coq.micromega.ZMicromega]
Zgcd_pol [definition, in Coq.micromega.ZMicromega]
Zgcd_alt [library]
Zge_left [lemma, in Coq.ZArith.auxiliary]
Zge_trans [lemma, in Coq.ZArith.Zorder]
Zge_iff_le [abbreviation, in Coq.ZArith.Zorder]
Zge_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zge_cases [lemma, in Coq.ZArith.Zbool]
Zge_bool [abbreviation, in Coq.ZArith.Zbool]
Zge_compare [lemma, in Coq.ZArith.Zcompare]
Zgt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zgt_left_gt [lemma, in Coq.ZArith.auxiliary]
Zgt_left [lemma, in Coq.ZArith.auxiliary]
Zgt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zgt_succ_gt_or_eq [lemma, in Coq.ZArith.Zorder]
Zgt_pos_0 [lemma, in Coq.ZArith.Zorder]
Zgt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zgt_succ_pred [lemma, in Coq.ZArith.Zorder]
Zgt_succ_le [lemma, in Coq.ZArith.Zorder]
Zgt_le_succ [lemma, in Coq.ZArith.Zorder]
Zgt_succ [lemma, in Coq.ZArith.Zorder]
Zgt_le_trans [lemma, in Coq.ZArith.Zorder]
Zgt_trans [lemma, in Coq.ZArith.Zorder]
Zgt_irrefl [lemma, in Coq.ZArith.Zorder]
Zgt_asym [lemma, in Coq.ZArith.Zorder]
Zgt_not_le [lemma, in Coq.ZArith.Zorder]
Zgt_iff_lt [abbreviation, in Coq.ZArith.Zorder]
Zgt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zgt_is_gt_bool [lemma, in Coq.ZArith.Zbool]
Zgt_cases [lemma, in Coq.ZArith.Zbool]
Zgt_bool [abbreviation, in Coq.ZArith.Zbool]
Zgt_compare [lemma, in Coq.ZArith.Zcompare]
Zhints [library]
Zify [library]
ZifyBool [library]
ZifyClasses [library]
ZifyComparison [library]
ZifyInst [library]
ZifyN [library]
ZifyNat [library]
ZifyPow [library]
ZifySint63 [library]
ZifyUint63 [library]
Zind [abbreviation, in Coq.ZArith.BinInt]
ZintNeg [constructor, in Coq.Reals.Rfunctions]
ZintNull [constructor, in Coq.Reals.Rfunctions]
ZintPos [constructor, in Coq.Reals.Rfunctions]
Zip [section, in Coq.Lists.Streams]
zipWith [definition, in Coq.Lists.Streams]
Zip.A [variable, in Coq.Lists.Streams]
Zip.B [variable, in Coq.Lists.Streams]
Zip.C [variable, in Coq.Lists.Streams]
Zip.f [variable, in Coq.Lists.Streams]
Zis_gcd_gcd [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_mult [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_bezout [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_uniqueness_apart_sign [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid2 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid [abbreviation, in Coq.ZArith.Znumtheory]
Zis_gcd_unique [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_0_abs [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_opp [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_minus [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_refl [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_1 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_0 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_sym [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_sind [definition, in Coq.ZArith.Znumtheory]
Zis_gcd_rec [definition, in Coq.ZArith.Znumtheory]
Zis_gcd_ind [definition, in Coq.ZArith.Znumtheory]
Zis_gcd_rect [definition, in Coq.ZArith.Znumtheory]
Zis_gcd_intro [constructor, in Coq.ZArith.Znumtheory]
Zis_gcd [inductive, in Coq.ZArith.Znumtheory]
ZLcm [library]
ZLcmProp [module, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_lcm_iff [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_lcm_eq_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_div [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_lcm_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_lcm_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_quot_mul_exact [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.divide_div_mul_exact [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_1_lcm_mul [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_div_swap [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_rem [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_mod [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_quot_gcd [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_div_gcd [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_quot_factor [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.gcd_div_factor [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm [definition, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_mul_mono_r_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_mul_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_mul_mono_l_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_mul_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_diag [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_abs_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_abs_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_eq_0 [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_diag_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_1_r_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_1_l_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_unique_alt [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_unique [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_divide_iff [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_comm [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_least [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_equiv2 [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_equiv1 [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.lcm_wd [instance, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.mod_divide [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.quot_div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.quot_div [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.quot_div_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.rem_mod_eq_0 [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.rem_divide [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.rem_mod [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
ZLcmProp.rem_mod_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZLcm]
Zlength [definition, in Coq.ZArith.Zcomplements]
Zlength_nil_inv [lemma, in Coq.ZArith.Zcomplements]
Zlength_cons [lemma, in Coq.ZArith.Zcomplements]
Zlength_nil [lemma, in Coq.ZArith.Zcomplements]
Zlength_correct [lemma, in Coq.ZArith.Zcomplements]
Zlength_properties.A [variable, in Coq.ZArith.Zcomplements]
Zlength_properties [section, in Coq.ZArith.Zcomplements]
Zlength_aux [definition, in Coq.ZArith.Zcomplements]
Zle_max_compat_l [abbreviation, in Coq.ZArith.Zmax]
Zle_max_compat_r [abbreviation, in Coq.ZArith.Zmax]
Zle_min_compat_l [abbreviation, in Coq.ZArith.Zmin]
Zle_min_compat_r [abbreviation, in Coq.ZArith.Zmin]
Zle_mult_approx [lemma, in Coq.ZArith.auxiliary]
Zle_left_rev [lemma, in Coq.ZArith.auxiliary]
Zle_left [lemma, in Coq.ZArith.auxiliary]
Zle_minus_le_0 [lemma, in Coq.ZArith.Zorder]
Zle_0_minus_le [lemma, in Coq.ZArith.Zorder]
Zle_plus_swap [abbreviation, in Coq.ZArith.Zorder]
Zle_0_nat [lemma, in Coq.ZArith.Zorder]
Zle_0_pos [lemma, in Coq.ZArith.Zorder]
Zle_neg_pos [lemma, in Coq.ZArith.Zorder]
Zle_succ_le [lemma, in Coq.ZArith.Zorder]
Zle_le_succ [abbreviation, in Coq.ZArith.Zorder]
Zle_pred [abbreviation, in Coq.ZArith.Zorder]
Zle_succ [abbreviation, in Coq.ZArith.Zorder]
Zle_succ_gt [lemma, in Coq.ZArith.Zorder]
Zle_lt_succ [lemma, in Coq.ZArith.Zorder]
Zle_gt_succ [lemma, in Coq.ZArith.Zorder]
Zle_gt_trans [lemma, in Coq.ZArith.Zorder]
Zle_or_lt [abbreviation, in Coq.ZArith.Zorder]
Zle_lt_or_eq [lemma, in Coq.ZArith.Zorder]
Zle_lt_or_eq_iff [abbreviation, in Coq.ZArith.Zorder]
Zle_antisym [abbreviation, in Coq.ZArith.Zorder]
Zle_not_gt [lemma, in Coq.ZArith.Zorder]
Zle_not_lt [lemma, in Coq.ZArith.Zorder]
Zle_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_bool_plus_mono [lemma, in Coq.ZArith.Zbool]
Zle_bool_total [definition, in Coq.ZArith.Zbool]
Zle_bool_trans [lemma, in Coq.ZArith.Zbool]
Zle_bool_antisym [lemma, in Coq.ZArith.Zbool]
Zle_bool_refl [abbreviation, in Coq.ZArith.Zbool]
Zle_imp_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_bool_imp_le [lemma, in Coq.ZArith.Zbool]
Zle_cases [lemma, in Coq.ZArith.Zbool]
Zle_bool [abbreviation, in Coq.ZArith.Zbool]
Zle_compare [lemma, in Coq.ZArith.Zcompare]
Zle_Qle [lemma, in Coq.QArith.QArith_base]
ZLt [library]
Zlt_le_add_1 [lemma, in Coq.micromega.Ztac]
Zlt_lower_bound_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_lower_bound_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_0_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_0_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_left [lemma, in Coq.ZArith.auxiliary]
Zlt_left_lt [lemma, in Coq.ZArith.auxiliary]
Zlt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zlt_O_minus_lt [abbreviation, in Coq.ZArith.Zorder]
Zlt_0_minus_lt [lemma, in Coq.ZArith.Zorder]
Zlt_minus_simpl_swap [abbreviation, in Coq.ZArith.Zorder]
Zlt_plus_swap [abbreviation, in Coq.ZArith.Zorder]
Zlt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zlt_neg_0 [lemma, in Coq.ZArith.Zorder]
Zlt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zlt_succ_pred [lemma, in Coq.ZArith.Zorder]
Zlt_lt_succ [abbreviation, in Coq.ZArith.Zorder]
Zlt_succ_le [lemma, in Coq.ZArith.Zorder]
Zlt_le_succ [lemma, in Coq.ZArith.Zorder]
Zlt_pred [abbreviation, in Coq.ZArith.Zorder]
Zlt_succ [abbreviation, in Coq.ZArith.Zorder]
Zlt_le_weak [abbreviation, in Coq.ZArith.Zorder]
Zlt_not_eq [abbreviation, in Coq.ZArith.Zorder]
Zlt_asym [abbreviation, in Coq.ZArith.Zorder]
Zlt_not_le [lemma, in Coq.ZArith.Zorder]
Zlt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zlt_is_lt_bool [lemma, in Coq.ZArith.Zbool]
Zlt_cases [lemma, in Coq.ZArith.Zbool]
Zlt_bool [abbreviation, in Coq.ZArith.Zbool]
Zlt_cotrans_neg [lemma, in Coq.ZArith.ZArith_dec]
Zlt_cotrans_pos [lemma, in Coq.ZArith.ZArith_dec]
Zlt_cotrans [lemma, in Coq.ZArith.ZArith_dec]
Zlt_compare [lemma, in Coq.ZArith.Zcompare]
Zlt_Qlt [lemma, in Coq.QArith.QArith_base]
ZL0 [lemma, in Coq.ZArith.BinInt]
ZL4 [abbreviation, in Coq.PArith.Pnat]
ZL6 [lemma, in Coq.PArith.Pnat]
Zmax [library]
ZMaxMin [library]
ZMaxMinProp [module, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.add_min_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.add_min_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.add_max_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.add_max_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_min_distr_nonpos_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_min_distr_nonpos_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_max_distr_nonpos_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_max_distr_nonpos_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_min_distr_nonneg_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_min_distr_nonneg_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_max_distr_nonneg_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.mul_max_distr_nonneg_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.opp_min_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.opp_max_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.pred_min_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.pred_max_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.sub_min_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.sub_min_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.sub_max_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.sub_max_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.succ_min_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZMaxMinProp.succ_max_distr [lemma, in Coq.Numbers.Integer.Abstract.ZMaxMin]
ZmaxSpec [instance, in Coq.micromega.ZifyInst]
Zmax_left [lemma, in Coq.ZArith.Zmax]
Zmax_spec [lemma, in Coq.ZArith.Zmax]
Zmax_le_prime_inf [abbreviation, in Coq.ZArith.Zmax]
Zmax_irreducible_inf [abbreviation, in Coq.ZArith.Zmax]
Zmax_plus [abbreviation, in Coq.ZArith.Zmax]
Zmax_SS [abbreviation, in Coq.ZArith.Zmax]
Zmax_le_prime [abbreviation, in Coq.ZArith.Zmax]
Zmax_irreducible_dec [abbreviation, in Coq.ZArith.Zmax]
Zmax_n_n [abbreviation, in Coq.ZArith.Zmax]
Zmax_idempotent [abbreviation, in Coq.ZArith.Zmax]
Zmax_right [abbreviation, in Coq.ZArith.Zmax]
Zmax_min_modular_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax_min_distr_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax_min_absorption_r_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax1 [abbreviation, in Coq.ZArith.Zmax]
Zmax2 [abbreviation, in Coq.ZArith.Zmax]
ZMicromega [library]
Zmin [library]
Zminmax [library]
ZminSpec [instance, in Coq.micromega.ZifyInst]
Zminus [abbreviation, in Coq.ZArith.BinInt]
Zminus_eq [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_r [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_l_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_l [lemma, in Coq.ZArith.BinInt]
Zminus_succ_l [lemma, in Coq.ZArith.BinInt]
Zminus_diag_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_0_l_reverse [lemma, in Coq.ZArith.BinInt]
Zminus_plus [abbreviation, in Coq.ZArith.BinInt]
Zminus_succ_r [abbreviation, in Coq.ZArith.BinInt]
Zminus_plus_distr [abbreviation, in Coq.ZArith.BinInt]
Zminus_diag [abbreviation, in Coq.ZArith.BinInt]
Zminus_0_r [abbreviation, in Coq.ZArith.BinInt]
Zminus_eqm [instance, in Coq.ZArith.Zdiv]
Zminus_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zminus_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zminus_mod [lemma, in Coq.ZArith.Zdiv]
Zmin_le_prime_inf [lemma, in Coq.ZArith.Zmin]
Zmin_or [abbreviation, in Coq.ZArith.Zmin]
Zmin_irreducible [lemma, in Coq.ZArith.Zmin]
Zmin_spec [lemma, in Coq.ZArith.Zmin]
Zmin_plus [abbreviation, in Coq.ZArith.Zmin]
Zmin_SS [abbreviation, in Coq.ZArith.Zmin]
Zmin_irreducible_inf [abbreviation, in Coq.ZArith.Zmin]
Zmin_n_n [abbreviation, in Coq.ZArith.Zmin]
Zmin_idempotent [abbreviation, in Coq.ZArith.Zmin]
Zmin_max_modular_r [abbreviation, in Coq.ZArith.Zminmax]
Zmin_max_distr_r [abbreviation, in Coq.ZArith.Zminmax]
Zmin_max_absorption_r_r [abbreviation, in Coq.ZArith.Zminmax]
Zmisc [library]
Zmod [abbreviation, in Coq.ZArith.Zdiv]
Zmod_POS_correct [lemma, in Coq.ZArith.Zdiv]
Zmod_POS [definition, in Coq.ZArith.Zdiv]
Zmod_even [lemma, in Coq.ZArith.Zdiv]
Zmod_odd [lemma, in Coq.ZArith.Zdiv]
Zmod_divides [lemma, in Coq.ZArith.Zdiv]
Zmod_div [lemma, in Coq.ZArith.Zdiv]
Zmod_eqm [lemma, in Coq.ZArith.Zdiv]
Zmod_mod [lemma, in Coq.ZArith.Zdiv]
Zmod_opp_opp [lemma, in Coq.ZArith.Zdiv]
Zmod_le [lemma, in Coq.ZArith.Zdiv]
Zmod_small [lemma, in Coq.ZArith.Zdiv]
Zmod_1_l [lemma, in Coq.ZArith.Zdiv]
Zmod_1_r [lemma, in Coq.ZArith.Zdiv]
Zmod_0_r [lemma, in Coq.ZArith.Zdiv]
Zmod_0_l [lemma, in Coq.ZArith.Zdiv]
Zmod_unique [lemma, in Coq.ZArith.Zdiv]
Zmod_unique_full [lemma, in Coq.ZArith.Zdiv]
Zmod_eq [lemma, in Coq.ZArith.Zdiv]
Zmod_eq_full [lemma, in Coq.ZArith.Zdiv]
Zmod_neg_bound [abbreviation, in Coq.ZArith.Zdiv]
Zmod_pos_bound [abbreviation, in Coq.ZArith.Zdiv]
Zmod_POS_bound [abbreviation, in Coq.ZArith.Zdiv]
Zmod_divide_minus [lemma, in Coq.ZArith.Znumtheory]
Zmod_div_mod [lemma, in Coq.ZArith.Znumtheory]
Zmod_divide [lemma, in Coq.ZArith.Znumtheory]
Zmod_distr [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
Zmod' [definition, in Coq.ZArith.Zdiv]
Zmod'_correct [lemma, in Coq.ZArith.Zdiv]
zmon [constructor, in Coq.setoid_ring.Ring_polynom]
zmon [constructor, in Coq.micromega.EnvRing]
zmon_pred_ok [lemma, in Coq.setoid_ring.Ring_polynom]
zmon_pred [definition, in Coq.setoid_ring.Ring_polynom]
zmon_pred_ok [lemma, in Coq.micromega.EnvRing]
zmon_pred [definition, in Coq.micromega.EnvRing]
ZMORPHISM [section, in Coq.setoid_ring.Ncring_initial]
ZMORPHISM [section, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ALMOST_RING.ARth [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ALMOST_RING [section, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ARth [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.R [variable, in Coq.setoid_ring.Ncring_initial]
ZMORPHISM.R [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.radd [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.req [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.Reqe [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.rI [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.rmul [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.rO [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ropp [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.Rsth [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.rsub [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.Rth [variable, in Coq.setoid_ring.InitialRing]
[ _ ] (ZMORPHISM) [notation, in Coq.setoid_ring.Ncring_initial]
_ == _ [notation, in Coq.setoid_ring.InitialRing]
_ - _ [notation, in Coq.setoid_ring.InitialRing]
_ * _ [notation, in Coq.setoid_ring.InitialRing]
_ + _ [notation, in Coq.setoid_ring.InitialRing]
- _ [notation, in Coq.setoid_ring.InitialRing]
0 [notation, in Coq.setoid_ring.InitialRing]
1 [notation, in Coq.setoid_ring.InitialRing]
[ _ ] [notation, in Coq.setoid_ring.InitialRing]
ZMul [library]
ZMulOrder [library]
ZMulOrderProp [module, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.eq_mul_1 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.le_mul_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.le_mul_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.le_0_square [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.le_mul_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.le_0_mul [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_m1_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_1_mul_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_m1_pos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_m1_neg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_1_mul_neg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.lt_mul_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_eq_1 [definition, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_nonpos [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_nonneg [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_neg [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_pos [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_nonpos_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_nonneg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_nonpos_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_le_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.mul_lt_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.nlt_square_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.square_le_simpl_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.square_lt_simpl_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.square_le_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderProp.square_lt_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulProp [module, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_sub_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_sub_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_opp_comm [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulProp.mul_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
Zmult [abbreviation, in Coq.ZArith.BinInt]
Zmult_succ_l_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_succ_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_minus_distr_l [lemma, in Coq.ZArith.BinInt]
Zmult_integral_l [lemma, in Coq.ZArith.BinInt]
Zmult_integral [lemma, in Coq.ZArith.BinInt]
Zmult_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_succ_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_succ_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_reg_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_reg_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_minus_distr_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_plus_distr_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_plus_distr_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_opp_comm [abbreviation, in Coq.ZArith.BinInt]
Zmult_opp_opp [abbreviation, in Coq.ZArith.BinInt]
Zmult_1_inversion_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_permute [abbreviation, in Coq.ZArith.BinInt]
Zmult_assoc [abbreviation, in Coq.ZArith.BinInt]
Zmult_comm [abbreviation, in Coq.ZArith.BinInt]
Zmult_1_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_1_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_0_r [abbreviation, in Coq.ZArith.BinInt]
Zmult_0_l [abbreviation, in Coq.ZArith.BinInt]
Zmult_power [lemma, in Coq.ZArith.Zpow_facts]
Zmult_eqm [instance, in Coq.ZArith.Zdiv]
Zmult_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zmult_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zmult_mod [lemma, in Coq.ZArith.Zdiv]
Zmult_mod_distr_r [lemma, in Coq.ZArith.Zdiv]
Zmult_mod_distr_l [lemma, in Coq.ZArith.Zdiv]
Zmult_le_approx [lemma, in Coq.ZArith.auxiliary]
Zmult_gt_0_reg_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_lt_O_compat [abbreviation, in Coq.ZArith.Zorder]
Zmult_lt_0_compat [abbreviation, in Coq.ZArith.Zorder]
Zmult_le_0_compat [abbreviation, in Coq.ZArith.Zorder]
Zmult_lt_compat2 [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat [lemma, in Coq.ZArith.Zorder]
Zmult_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_ge_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat [lemma, in Coq.ZArith.Zorder]
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_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_rem_idemp_r [lemma, in Coq.ZArith.Zquot]
Zmult_rem_idemp_l [lemma, in Coq.ZArith.Zquot]
Zmult_rem [lemma, in Coq.ZArith.Zquot]
Zmult_rem_distr_r [lemma, in Coq.ZArith.Zquot]
Zmult_rem_distr_l [lemma, in Coq.ZArith.Zquot]
Zmult_one [lemma, in Coq.ZArith.Znumtheory]
Zmult_divide_compat_r [abbreviation, in Coq.ZArith.Znumtheory]
Zmult_divide_compat_l [abbreviation, in Coq.ZArith.Znumtheory]
Zmult_compare_compat_r [lemma, in Coq.ZArith.Zcompare]
Zmult_compare_compat_l [lemma, in Coq.ZArith.Zcompare]
ZN [definition, in Coq.setoid_ring.Ncring]
Znat [library]
ZNatPairs [library]
Zne [definition, in Coq.ZArith.BinInt]
Zneg [abbreviation, in Coq.ZArith.BinInt]
Zneg [constructor, in Coq.Numbers.BinNums]
Zneg_plus_distr [abbreviation, in Coq.ZArith.BinInt]
Zneg_xO [abbreviation, in Coq.ZArith.BinInt]
Zneg_xI [abbreviation, in Coq.ZArith.BinInt]
Zneq_bool [definition, in Coq.ZArith.Zbool]
Zne_left [lemma, in Coq.ZArith.auxiliary]
Znot_le_succ [lemma, in Coq.ZArith.Zorder]
Znot_le_gt [lemma, in Coq.ZArith.Zorder]
Znot_gt_le [lemma, in Coq.ZArith.Zorder]
Znot_lt_ge [lemma, in Coq.ZArith.Zorder]
Znot_ge_lt [lemma, in Coq.ZArith.Zorder]
ZNpower [lemma, in Coq.micromega.ZMicromega]
Znumtheory [library]
ZnZ [module, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.add [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.add_mul_div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.add_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.add_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.add_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.compare [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.digits [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.div_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.div21 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.eq0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.gcd [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.gcd_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.head0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.is_even [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.land [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.lor [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.lxor [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.minus_one [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.modulo [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.modulo_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.mul [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.mul_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.of_Z_correct [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.of_Z [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.of_pos_correct [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Of_Z.specs [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Of_Z.ops [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Of_Z.t [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Of_Z [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.of_pos [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.one [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.opp [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.opp_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.opp_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Ops [record, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.OW [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.OW' [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.pos_mod [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.pred [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.pred_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Specs [record, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Specs [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Specs.ops [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Specs.t [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.Specs.wB [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[+| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[-| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[|| _ ||] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_WW [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_OW [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_WO [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_lxor [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_land [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_lor [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sqrt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sqrt2 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_is_even [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_pos_mod [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_add_mul_div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_tail0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_tail00 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_head0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_head00 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_gcd [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_gcd_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_modulo [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_modulo_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_div_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_div21 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_square_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_mul [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_mul_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sub_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sub [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_pred [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sub_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_sub_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_pred_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_add_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_add [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_succ [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_add_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_add_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_succ_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_opp_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_opp [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_opp_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_eq0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_compare [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_m1 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_1 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_more_than_1_digit [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_zdigits [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_of_pos [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.spec_to_Z [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sqrt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sqrt2 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.square_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sub [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sub_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sub_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.sub_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.succ [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.succ_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.tail0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.to_Z [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WO [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WO' [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW' [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW.ops [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW.specs [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW.t [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.WW.wB [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.zdigits [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
ZnZ.zero [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zn2z [inductive, in Coq.Numbers.Cyclic.Abstract.DoubleType]
zn2z_to_Z [definition, in Coq.Numbers.Cyclic.Abstract.DoubleType]
Zodd [definition, in Coq.ZArith.Zeven]
Zodd_mult_Zodd [lemma, in Coq.ZArith.Zeven]
Zodd_plus_Zodd [lemma, in Coq.ZArith.Zeven]
Zodd_plus_Zeven [lemma, in Coq.ZArith.Zeven]
Zodd_2p_plus_1 [lemma, in Coq.ZArith.Zeven]
Zodd_ex [lemma, in Coq.ZArith.Zeven]
Zodd_quot2_neg [lemma, in Coq.ZArith.Zeven]
Zodd_quot2 [lemma, in Coq.ZArith.Zeven]
Zodd_div2 [lemma, in Coq.ZArith.Zeven]
Zodd_bool_pred [abbreviation, in Coq.ZArith.Zeven]
Zodd_bool_succ [abbreviation, in Coq.ZArith.Zeven]
Zodd_pred [lemma, in Coq.ZArith.Zeven]
Zodd_Sn [lemma, in Coq.ZArith.Zeven]
Zodd_not_Zeven [lemma, in Coq.ZArith.Zeven]
Zodd_dec [definition, in Coq.ZArith.Zeven]
Zodd_even_bool [lemma, in Coq.ZArith.Zeven]
Zodd_bool_iff [lemma, in Coq.ZArith.Zeven]
Zodd_bool [abbreviation, in Coq.ZArith.Zeven]
Zodd_ex_iff [lemma, in Coq.ZArith.Zeven]
Zodd_equiv [lemma, in Coq.ZArith.Zeven]
Zodd_mod [lemma, in Coq.ZArith.Zdiv]
Zodd_rem [lemma, in Coq.ZArith.Zquot]
Zone_min_pos [lemma, in Coq.ZArith.Zbool]
Zone_pos [lemma, in Coq.ZArith.Zbool]
Zone_divide [abbreviation, in Coq.ZArith.Znumtheory]
Zopp_mult_distr_r [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_l [lemma, in Coq.ZArith.BinInt]
Zopp_neg [abbreviation, in Coq.ZArith.BinInt]
Zopp_eq_mult_neg_1 [abbreviation, in Coq.ZArith.BinInt]
Zopp_mult_distr_l_reverse [abbreviation, in Coq.ZArith.BinInt]
Zopp_plus_distr [abbreviation, in Coq.ZArith.BinInt]
Zopp_eqm [instance, in Coq.ZArith.Zdiv]
Zops [instance, in Coq.setoid_ring.Ncring_initial]
Zorder [library]
ZOrderProp [module, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.le_pred_lt_succ [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.le_succ_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.le_pred_lt [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.le_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.le_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_m1_r [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_pred_lt_succ [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_succ_lt_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_pred_lt [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_lt_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_pred_le [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.lt_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.neg_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.neg_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.neq_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.nle_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.nonpos_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.nonpos_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.pred_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderProp.pred_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZPairsAxiomsMod [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.add [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.add_succ_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.add_0_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.add_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.bi_induction [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.eq [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.eq_equiv [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Induction [section, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Induction.A [variable, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Induction.A_wd [variable, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.le [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_nge [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_succ_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_irrefl [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_eq_cases [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_succ_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_0_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_comm [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.NProp [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.one [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.one_succ [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp_succ [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp_0 [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pair_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pred [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pred_succ [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pred_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub_succ_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub_0_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub_add_opp [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.succ [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.succ_pred [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.succ_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.t [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.two [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.two_succ [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.zero [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.add [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.eq [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.le [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.lt [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.max [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.min [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.mul [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.one [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.opp [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.pred [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.sub [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.succ [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.t [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.two [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.Z.zero [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ <= _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ < _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ * _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ - _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ + _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ ~= _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ == _ (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
0 (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
1 (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
2 (NScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ <= _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ < _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ * _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ - _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ + _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ ~= _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
_ == _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
- _ (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
0 (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
1 (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
2 (ZScope) [notation, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZParity [library]
ZParityProp [module, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.even_sub [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.even_opp [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.even_pred [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.odd_sub [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.odd_opp [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
ZParityProp.odd_pred [lemma, in Coq.Numbers.Integer.Abstract.ZParity]
Zplus [abbreviation, in Coq.ZArith.BinInt]
Zplus_diag_eq_mult_2 [lemma, in Coq.ZArith.BinInt]
Zplus_minus [lemma, in Coq.ZArith.BinInt]
Zplus_minus_eq [lemma, in Coq.ZArith.BinInt]
Zplus_eq_compat [lemma, in Coq.ZArith.BinInt]
Zplus_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_succ_r [abbreviation, in Coq.ZArith.BinInt]
Zplus_succ_r_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_succ_comm [abbreviation, in Coq.ZArith.BinInt]
Zplus_succ_l [abbreviation, in Coq.ZArith.BinInt]
Zplus_reg_l [abbreviation, in Coq.ZArith.BinInt]
Zplus_permute [abbreviation, in Coq.ZArith.BinInt]
Zplus_assoc [abbreviation, in Coq.ZArith.BinInt]
Zplus_opp_l [abbreviation, in Coq.ZArith.BinInt]
Zplus_opp_r [abbreviation, in Coq.ZArith.BinInt]
Zplus_comm [abbreviation, in Coq.ZArith.BinInt]
Zplus_0_r [abbreviation, in Coq.ZArith.BinInt]
Zplus_0_l [abbreviation, in Coq.ZArith.BinInt]
Zplus_max_distr_r [abbreviation, in Coq.ZArith.Zmax]
Zplus_max_distr_l [abbreviation, in Coq.ZArith.Zmax]
Zplus_min_distr_r [abbreviation, in Coq.ZArith.Zmin]
Zplus_eqm [instance, in Coq.ZArith.Zdiv]
Zplus_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zplus_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zplus_mod [lemma, in Coq.ZArith.Zdiv]
Zplus_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_gt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_lt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_0_compat [abbreviation, in Coq.ZArith.Zorder]
Zplus_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_lt_compat [abbreviation, in Coq.ZArith.Zorder]
Zplus_le_compat [abbreviation, in Coq.ZArith.Zorder]
Zplus_le_lt_compat [abbreviation, in Coq.ZArith.Zorder]
Zplus_lt_le_compat [abbreviation, in Coq.ZArith.Zorder]
Zplus_rem_idemp_r [lemma, in Coq.ZArith.Zquot]
Zplus_rem_idemp_l [lemma, in Coq.ZArith.Zquot]
Zplus_rem [lemma, in Coq.ZArith.Zquot]
Zplus_compare_compat [lemma, in Coq.ZArith.Zcompare]
ZPminus [abbreviation, in Coq.ZArith.BinInt]
Zpos [abbreviation, in Coq.ZArith.BinInt]
Zpos [constructor, in Coq.Numbers.BinNums]
Zpos_eq_iff [lemma, in Coq.ZArith.BinInt]
Zpos_eq [lemma, in Coq.ZArith.BinInt]
Zpos_plus_distr [abbreviation, in Coq.ZArith.BinInt]
Zpos_eq_rev [abbreviation, in Coq.ZArith.BinInt]
Zpos_minus_morphism [abbreviation, in Coq.ZArith.BinInt]
Zpos_mult_morphism [abbreviation, in Coq.ZArith.BinInt]
Zpos_succ_morphism [abbreviation, in Coq.ZArith.BinInt]
Zpos_xO [abbreviation, in Coq.ZArith.BinInt]
Zpos_xI [abbreviation, in Coq.ZArith.BinInt]
Zpos_max_1 [lemma, in Coq.ZArith.Zmax]
Zpos_minus [abbreviation, in Coq.ZArith.Zmax]
Zpos_max [abbreviation, in Coq.ZArith.Zmax]
Zpos_min_1 [lemma, in Coq.ZArith.Zmin]
Zpos_min [abbreviation, in Coq.ZArith.Zmin]
Zpos_eq_Z_of_nat_o_nat_of_P [abbreviation, in Coq.ZArith.Znat]
Zpos_P_of_succ_nat [lemma, in Coq.ZArith.Znat]
ZPow [library]
Zpower [abbreviation, in Coq.ZArith.Zpow_def]
Zpower [library]
Zpower_nat_powerRZ_absolu [lemma, in Coq.Reals.Rfunctions]
Zpower_pos_powerRZ [lemma, in Coq.Reals.Rfunctions]
Zpower_nat_powerRZ [lemma, in Coq.Reals.Rfunctions]
Zpower_NR0 [lemma, in Coq.Reals.Rfunctions]
Zpower_divide [lemma, in Coq.ZArith.Zpow_facts]
Zpower_mod [lemma, in Coq.ZArith.Zpow_facts]
Zpower_nat_Zpower [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone_inv [lemma, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone3 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_gt_1 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_lt_monotone [lemma, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone [lemma, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone2 [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_mult [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_Zsucc [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_Zabs [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_ge_0 [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_gt_0 [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_2 [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_0_r [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_0_l [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_1_l [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_1_r [abbreviation, in Coq.ZArith.Zpow_facts]
Zpower_pos_pos [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_0_l [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_1_l [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_1_r [lemma, in Coq.ZArith.Zpow_facts]
Zpower_theory [lemma, in Coq.ZArith.Zpow_def]
Zpower_Ppow [abbreviation, in Coq.ZArith.Zpow_def]
Zpower_neg_r [abbreviation, in Coq.ZArith.Zpow_def]
Zpower_succ_r [abbreviation, in Coq.ZArith.Zpow_def]
Zpower_0_r [abbreviation, in Coq.ZArith.Zpow_def]
Zpower_pos [abbreviation, in Coq.ZArith.Zpow_def]
Zpower_exp [lemma, in Coq.ZArith.Zpower]
Zpower_pos_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_nat_Zpower [lemma, in Coq.ZArith.Zpower]
Zpower_nat_Z [lemma, in Coq.ZArith.Zpower]
Zpower_pos_nat [lemma, in Coq.ZArith.Zpower]
Zpower_nat_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_nat_succ_r [lemma, in Coq.ZArith.Zpower]
Zpower_nat_0_r [lemma, in Coq.ZArith.Zpower]
Zpower_nat [definition, in Coq.ZArith.Zpower]
Zpower_alt_Ppow [lemma, in Coq.ZArith.Zpow_alt]
Zpower_alt_neg_r [lemma, in Coq.ZArith.Zpow_alt]
Zpower_alt_succ_r [lemma, in Coq.ZArith.Zpow_alt]
Zpower_alt_0_r [lemma, in Coq.ZArith.Zpow_alt]
Zpower_equiv [lemma, in Coq.ZArith.Zpow_alt]
Zpower_alt [definition, in Coq.ZArith.Zpow_alt]
Zpower_Qpower [lemma, in Coq.QArith.Qpower]
Zpower2_Psize [lemma, in Coq.ZArith.Zpow_facts]
Zpower2_le_lin [lemma, in Coq.ZArith.Zpow_facts]
Zpower2_lt_lin [lemma, in Coq.ZArith.Zpow_facts]
ZPowProp [module, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.abs_pow [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.even_pow [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.odd_pow [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_odd_sgn [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_odd_abs_sgn [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_even_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_even_abs [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_opp_odd [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_opp_even [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
ZPowProp.pow_twice_r [lemma, in Coq.Numbers.Integer.Abstract.ZPow]
Zpow_mod_correct [lemma, in Coq.ZArith.Zpow_facts]
Zpow_mod_pos_correct [lemma, in Coq.ZArith.Zpow_facts]
Zpow_mod [definition, in Coq.ZArith.Zpow_facts]
Zpow_mod_pos [definition, in Coq.ZArith.Zpow_facts]
Zpow_def [library]
Zpow_facts [library]
Zpow_alt [library]
Zpred_succ [lemma, in Coq.ZArith.BinInt]
ZProperties [library]
ZQuot [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Zquot [library]
ZQuotProp [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.add_rem [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.add_rem_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.add_rem_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mod_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_rem [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_rem_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_rem_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_rem_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_rem_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_succ_quot_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_pred_quot_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_pred_quot_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_succ_quot_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_quot_ge [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.mul_quot_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.NZQuot [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.mod_bound_pos [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div_mod [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.mod_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.modulo [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div.div [definition, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div.Quot2Div [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.Private_Div [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_quot [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_abs [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_abs_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_abs_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_unique_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_rem_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.quot_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_quot [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_rem [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_bound_abs [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_abs [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_abs_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_abs_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_sign [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_sign_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_sign_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZQuotProp.rem_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
Zquotrem_Zdiv_eucl_pos [lemma, in Coq.ZArith.Zquot]
Zquot_Zdiv_pos [lemma, in Coq.ZArith.Zquot]
Zquot_mult_le [lemma, in Coq.ZArith.Zquot]
Zquot_Zquot [lemma, in Coq.ZArith.Zquot]
Zquot_mult_cancel_l [lemma, in Coq.ZArith.Zquot]
Zquot_mult_cancel_r [lemma, in Coq.ZArith.Zquot]
Zquot_sgn [lemma, in Coq.ZArith.Zquot]
Zquot_le_lower_bound [lemma, in Coq.ZArith.Zquot]
Zquot_lt_upper_bound [lemma, in Coq.ZArith.Zquot]
Zquot_le_upper_bound [lemma, in Coq.ZArith.Zquot]
Zquot_unique_full [lemma, in Coq.ZArith.Zquot]
Zquot_mod_unique_full [lemma, in Coq.ZArith.Zquot]
Zquot_opp_opp [lemma, in Coq.ZArith.Zquot]
Zquot_opp_r [lemma, in Coq.ZArith.Zquot]
Zquot_opp_l [lemma, in Coq.ZArith.Zquot]
Zquot_0_l [lemma, in Coq.ZArith.Zquot]
Zquot_0_r [lemma, in Coq.ZArith.Zquot]
ZQuot' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Zquot2_quot [lemma, in Coq.ZArith.Zeven]
Zquot2_opp [lemma, in Coq.ZArith.Zeven]
Zquot2_odd_eqn [lemma, in Coq.ZArith.Zeven]
Zquot2_odd_remainder [lemma, in Coq.ZArith.Zquot]
Zr [instance, in Coq.setoid_ring.Ncring_initial]
Zred_factor6 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor5 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor4 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor3 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor2 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor1 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor0 [lemma, in Coq.omega.OmegaLemmas]
Zrel_prime_neq_mod_0 [lemma, in Coq.ZArith.Znumtheory]
Zrem_Zmod_zero [lemma, in Coq.ZArith.Zquot]
Zrem_Zmod_pos [lemma, in Coq.ZArith.Zquot]
Zrem_even [lemma, in Coq.ZArith.Zquot]
Zrem_odd [lemma, in Coq.ZArith.Zquot]
Zrem_divides [lemma, in Coq.ZArith.Zquot]
Zrem_rem [lemma, in Coq.ZArith.Zquot]
Zrem_le [lemma, in Coq.ZArith.Zquot]
Zrem_unique_full [lemma, in Coq.ZArith.Zquot]
Zrem_lt_neg_neg [lemma, in Coq.ZArith.Zquot]
Zrem_lt_neg_pos [lemma, in Coq.ZArith.Zquot]
Zrem_lt_pos_neg [lemma, in Coq.ZArith.Zquot]
Zrem_lt_pos_pos [lemma, in Coq.ZArith.Zquot]
Zrem_lt_neg [lemma, in Coq.ZArith.Zquot]
Zrem_lt_pos [lemma, in Coq.ZArith.Zquot]
Zrem_sgn2 [lemma, in Coq.ZArith.Zquot]
Zrem_sgn [lemma, in Coq.ZArith.Zquot]
Zrem_opp_opp [lemma, in Coq.ZArith.Zquot]
Zrem_opp_r [lemma, in Coq.ZArith.Zquot]
Zrem_opp_l [lemma, in Coq.ZArith.Zquot]
Zrem_0_l [lemma, in Coq.ZArith.Zquot]
Zrem_0_r [lemma, in Coq.ZArith.Zquot]
Zrem_lt [abbreviation, in Coq.ZArith.Zquot]
Zring_morph [lemma, in Coq.micromega.ZCoeff]
ZSgnAbs [library]
ZSgnAbsProp [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_sgn [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_square [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_mul [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_sub_triangle [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_triangle [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_le [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_lt [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_eq_cases [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_case [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_case_strong [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_spec [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_involutive [abbreviation, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_idemp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_or_opp_abs [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_eq_or_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_pos [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_0 [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_neq_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_eq_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_neq' [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_max [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.abs_wd [instance, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_sgn [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_abs [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_mul [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_neg_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_null_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_pos_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_0 [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_spec [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsProp.sgn_wd [instance, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZsgnSpec [instance, in Coq.micromega.ZifyInst]
Zsgn_spec [lemma, in Coq.ZArith.Zabs]
Zsgn_null [abbreviation, in Coq.ZArith.Zabs]
Zsgn_neg [abbreviation, in Coq.ZArith.Zabs]
Zsgn_pos [abbreviation, in Coq.ZArith.Zabs]
Zsgn_Zopp [abbreviation, in Coq.ZArith.Zabs]
Zsgn_Zmult [abbreviation, in Coq.ZArith.Zabs]
Zsgn_Zabs [abbreviation, in Coq.ZArith.Zabs]
Zsgn_m1 [abbreviation, in Coq.ZArith.Zcompare]
Zsgn_1 [abbreviation, in Coq.ZArith.Zcompare]
Zsgn_0 [abbreviation, in Coq.ZArith.Zcompare]
Zsor [lemma, in Coq.micromega.ZMicromega]
ZSORaddon [lemma, in Coq.micromega.ZMicromega]
Zsplit2 [lemma, in Coq.ZArith.Zeven]
Zsquare_correct [abbreviation, in Coq.ZArith.Zpow_facts]
Zsth [lemma, in Coq.setoid_ring.Ncring_initial]
Zsth [lemma, in Coq.setoid_ring.InitialRing]
Zsucc_eq_compat [lemma, in Coq.ZArith.BinInt]
Zsucc_pred [lemma, in Coq.ZArith.BinInt]
Zsucc_discr [abbreviation, in Coq.ZArith.BinInt]
Zsucc_lt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_le_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_gt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_gt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_lt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_le_compat [lemma, in Coq.ZArith.Zorder]
Zsucc'_discr [abbreviation, in Coq.ZArith.BinInt]
Ztac [library]
ZTautoChecker [definition, in Coq.micromega.ZMicromega]
ZTautoChecker_sound [lemma, in Coq.micromega.ZMicromega]
Zth [lemma, in Coq.setoid_ring.InitialRing]
ZtoN [definition, in Coq.setoid_ring.Field_theory]
Ztrichotomy [lemma, in Coq.ZArith.Zorder]
Ztrichotomy_inf [lemma, in Coq.ZArith.Zorder]
Ztriv_div_th [lemma, in Coq.setoid_ring.InitialRing]
Zunsat [definition, in Coq.micromega.ZMicromega]
Zunsat_sound [lemma, in Coq.micromega.ZMicromega]
ZWeakChecker [definition, in Coq.micromega.ZMicromega]
ZWeakChecker_sound [lemma, in Coq.micromega.ZMicromega]
ZweakTautoChecker [definition, in Coq.micromega.ZMicromega]
Zwf [definition, in Coq.ZArith.Zwf]
Zwf [library]
Zwf_up_well_founded [lemma, in Coq.ZArith.Zwf]
Zwf_up [definition, in Coq.ZArith.Zwf]
Zwf_well_founded [lemma, in Coq.ZArith.Zwf]
ZWitness [definition, in Coq.micromega.ZMicromega]
Z_as_DT [module, in Coq.Structures.DecidableTypeEx]
Z_one_zero [lemma, in Coq.nsatz.NsatzTactic]
Z_as_DT [module, in Coq.Structures.OrdersEx]
Z_as_OT [module, in Coq.Structures.OrdersEx]
Z_spec_sind [definition, in Coq.Reals.Rfunctions]
Z_spec_rec [definition, in Coq.Reals.Rfunctions]
Z_spec_ind [definition, in Coq.Reals.Rfunctions]
Z_spec_rect [definition, in Coq.Reals.Rfunctions]
Z_spec [inductive, in Coq.Reals.Rfunctions]
Z_ldexp_spec [lemma, in Coq.Floats.FloatLemmas]
Z_frexp_spec [lemma, in Coq.Floats.FloatLemmas]
Z_eq_mult [lemma, in Coq.ZArith.BinInt]
Z_ind [abbreviation, in Coq.ZArith.BinInt]
Z_rec [abbreviation, in Coq.ZArith.BinInt]
Z_rect [abbreviation, in Coq.ZArith.BinInt]
Z_of_N [abbreviation, in Coq.ZArith.BinInt]
Z_of_nat [abbreviation, in Coq.ZArith.BinInt]
Z_lt_induction [lemma, in Coq.ZArith.Wf_Z]
Z_lt_rec [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_set [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_prop [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_complete_inf [lemma, in Coq.ZArith.Wf_Z]
Z_of_nat_complete [lemma, in Coq.ZArith.Wf_Z]
Z_pos_sub_gt [lemma, in Coq.setoid_ring.Field_theory]
Z_of_nat_ltb_iff [lemma, in Coq.micromega.ZifyBool]
Z_of_nat_leb_iff [lemma, in Coq.micromega.ZifyBool]
Z_of_nat_eqb_iff [lemma, in Coq.micromega.ZifyBool]
Z_modulo_2 [lemma, in Coq.ZArith.Zeven]
Z_mod_zero_opp [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_2 [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_1 [lemma, in Coq.ZArith.Zdiv]
Z_mod_plus [lemma, in Coq.ZArith.Zdiv]
Z_div_mult [lemma, in Coq.ZArith.Zdiv]
Z_div_plus [lemma, in Coq.ZArith.Zdiv]
Z_div_same [lemma, in Coq.ZArith.Zdiv]
Z_mod_same [lemma, in Coq.ZArith.Zdiv]
Z_div_nz_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_div_zero_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_div_nz_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_div_zero_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_nz_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_mod_zero_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_mod_nz_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_zero_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_div_plus_full_l [lemma, in Coq.ZArith.Zdiv]
Z_div_plus_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_plus_full [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_full_2 [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_full_1 [lemma, in Coq.ZArith.Zdiv]
Z_mult_div_ge_neg [lemma, in Coq.ZArith.Zdiv]
Z_mult_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_div_le [lemma, in Coq.ZArith.Zdiv]
Z_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_div_lt [lemma, in Coq.ZArith.Zdiv]
Z_mod_nonneg_nonneg [lemma, in Coq.ZArith.Zdiv]
Z_div_nonneg_nonneg [lemma, in Coq.ZArith.Zdiv]
Z_div_ge0 [lemma, in Coq.ZArith.Zdiv]
Z_div_pos [lemma, in Coq.ZArith.Zdiv]
Z_div_mult_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_mult [lemma, in Coq.ZArith.Zdiv]
Z_mod_same_full [lemma, in Coq.ZArith.Zdiv]
Z_div_same_full [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_eq_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_neg [lemma, in Coq.ZArith.Zdiv]
Z_mod_lt [lemma, in Coq.ZArith.Zdiv]
Z_mod_remainder [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_full [lemma, in Coq.ZArith.Zdiv]
Z_div_mod [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_POS [lemma, in Coq.ZArith.Zdiv]
Z_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
Z_as_OT.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
Z_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
Z_as_OT [module, in Coq.Structures.OrderedTypeEx]
Z_as_Int.mult [abbreviation, in Coq.ZArith.Int]
Z_as_Int.minus [abbreviation, in Coq.ZArith.Int]
Z_as_Int.plus [abbreviation, in Coq.ZArith.Int]
Z_as_Int.i2z_ltb [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_leb [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_eqb [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_max [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_mul [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_sub [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_opp [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_add [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_3 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_2 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_1 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_0 [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z_eq [lemma, in Coq.ZArith.Int]
Z_as_Int.i2z [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.eq_dec [definition, in Coq.ZArith.Int]
Z_as_Int.leb [definition, in Coq.ZArith.Int]
Z_as_Int.ltb [definition, in Coq.ZArith.Int]
Z_as_Int.eqb [definition, in Coq.ZArith.Int]
Z_as_Int.max [definition, in Coq.ZArith.Int]
Z_as_Int.mul [definition, in Coq.ZArith.Int]
Z_as_Int.sub [definition, in Coq.ZArith.Int]
Z_as_Int.opp [definition, in Coq.ZArith.Int]
Z_as_Int.add [definition, in Coq.ZArith.Int]
Z_as_Int._3 [definition, in Coq.ZArith.Int]
Z_as_Int._2 [definition, in Coq.ZArith.Int]
Z_as_Int._1 [definition, in Coq.ZArith.Int]
Z_as_Int._0 [definition, in Coq.ZArith.Int]
Z_as_Int.t [definition, in Coq.ZArith.Int]
Z_as_Int [module, in Coq.ZArith.Int]
Z_of_of_Z [lemma, in Coq.Strings.BinaryString]
Z_inj_nat_inj [lemma, in Coq.Reals.Cauchy.ConstructiveExtra]
Z_inj_nat_id [lemma, in Coq.Reals.Cauchy.ConstructiveExtra]
Z_inj_nat_rev [definition, in Coq.Reals.Cauchy.ConstructiveExtra]
Z_inj_nat [definition, in Coq.Reals.Cauchy.ConstructiveExtra]
Z_noteq_bool [definition, in Coq.ZArith.Zbool]
Z_eq_bool [definition, in Coq.ZArith.Zbool]
Z_gt_le_bool [definition, in Coq.ZArith.Zbool]
Z_le_gt_bool [definition, in Coq.ZArith.Zbool]
Z_ge_lt_bool [definition, in Coq.ZArith.Zbool]
Z_lt_ge_bool [definition, in Coq.ZArith.Zbool]
Z_noteq_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_notzerop [lemma, in Coq.ZArith.ZArith_dec]
Z_zerop [lemma, in Coq.ZArith.ZArith_dec]
Z_dec' [lemma, in Coq.ZArith.ZArith_dec]
Z_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_le_lt_eq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_ge_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_gt_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_le_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_lt_le_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_lt_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_of_comparison_bound [lemma, in Coq.micromega.ZifyComparison]
Z_of_comparison [definition, in Coq.micromega.ZifyComparison]
Z_quot_plus_l [lemma, in Coq.ZArith.Zquot]
Z_quot_plus [lemma, in Coq.ZArith.Zquot]
Z_rem_plus [lemma, in Coq.ZArith.Zquot]
Z_quot_exact_full [lemma, in Coq.ZArith.Zquot]
Z_mult_quot_ge [lemma, in Coq.ZArith.Zquot]
Z_mult_quot_le [lemma, in Coq.ZArith.Zquot]
Z_quot_monotone [lemma, in Coq.ZArith.Zquot]
Z_quot_lt [lemma, in Coq.ZArith.Zquot]
Z_quot_pos [lemma, in Coq.ZArith.Zquot]
Z_rem_mult [lemma, in Coq.ZArith.Zquot]
Z_rem_same [lemma, in Coq.ZArith.Zquot]
Z_quot_mult [abbreviation, in Coq.ZArith.Zquot]
Z_quot_rem_eq [abbreviation, in Coq.ZArith.Zquot]
Z_sind [definition, in Coq.Numbers.BinNums]
Z_rec [definition, in Coq.Numbers.BinNums]
Z_ind [definition, in Coq.Numbers.BinNums]
Z_rect [definition, in Coq.Numbers.BinNums]
Z_R_minus [lemma, in Coq.Reals.RIneq]
Z_one_zero [lemma, in Coq.setoid_ring.Rings_Z]
z_of_exp [definition, in Coq.micromega.RMicromega]
Z_lt_abs_induction [lemma, in Coq.ZArith.Zcomplements]
Z_lt_abs_rec [lemma, in Coq.ZArith.Zcomplements]
Z_of_N_max [abbreviation, in Coq.ZArith.Znat]
Z_of_N_min [abbreviation, in Coq.ZArith.Znat]
Z_of_N_succ [abbreviation, in Coq.ZArith.Znat]
Z_of_N_minus [abbreviation, in Coq.ZArith.Znat]
Z_of_N_mult [abbreviation, in Coq.ZArith.Znat]
Z_of_N_plus [abbreviation, in Coq.ZArith.Znat]
Z_of_N_le_0 [abbreviation, in Coq.ZArith.Znat]
Z_of_N_abs [abbreviation, in Coq.ZArith.Znat]
Z_of_N_pos [abbreviation, in Coq.ZArith.Znat]
Z_of_N_gt_rev [abbreviation, in Coq.ZArith.Znat]
Z_of_N_ge_rev [abbreviation, in Coq.ZArith.Znat]
Z_of_N_lt_rev [abbreviation, in Coq.ZArith.Znat]
Z_of_N_le_rev [abbreviation, in Coq.ZArith.Znat]
Z_of_N_gt [abbreviation, in Coq.ZArith.Znat]
Z_of_N_ge [abbreviation, in Coq.ZArith.Znat]
Z_of_N_lt [abbreviation, in Coq.ZArith.Znat]
Z_of_N_le [abbreviation, in Coq.ZArith.Znat]
Z_of_N_gt_iff [abbreviation, in Coq.ZArith.Znat]
Z_of_N_ge_iff [abbreviation, in Coq.ZArith.Znat]
Z_of_N_lt_iff [abbreviation, in Coq.ZArith.Znat]
Z_of_N_le_iff [abbreviation, in Coq.ZArith.Znat]
Z_of_N_compare [abbreviation, in Coq.ZArith.Znat]
Z_of_N_eq_iff [abbreviation, in Coq.ZArith.Znat]
Z_of_N_eq_rev [abbreviation, in Coq.ZArith.Znat]
Z_of_N_eq [abbreviation, in Coq.ZArith.Znat]
Z_of_N_of_nat [abbreviation, in Coq.ZArith.Znat]
Z_of_nat_of_N [abbreviation, in Coq.ZArith.Znat]
Z_of_nat_of_P [abbreviation, in Coq.ZArith.Znat]
Z_nat_N [lemma, in Coq.ZArith.Znat]
Z_N_nat [lemma, in Coq.ZArith.Znat]
Z_0_1_more [lemma, in Coq.ZArith.Znumtheory]
Z_lt_neq [lemma, in Coq.ZArith.Znumtheory]
z_of_int [definition, in Coq.extraction.ExtrOcamlIntConv]
Z_evenE [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
Z_oddE [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
z_of_z [definition, in Coq.Numbers.AltBinNotations]
Z.abs [definition, in Coq.ZArith.BinIntDef]
Z.abs_N [definition, in Coq.ZArith.BinIntDef]
Z.abs_nat [definition, in Coq.ZArith.BinIntDef]
Z.abs_neq [lemma, in Coq.ZArith.BinInt]
Z.abs_eq [lemma, in Coq.ZArith.BinInt]
Z.adccarries [definition, in Coq.ZArith.Zbitwise]
Z.add [definition, in Coq.ZArith.BinIntDef]
Z.addcarries [definition, in Coq.ZArith.Zbitwise]
Z.addcarries_lor_land [lemma, in Coq.ZArith.Zbitwise]
Z.addcarries_ok [lemma, in Coq.ZArith.Zbitwise]
Z.addcarryeqn [lemma, in Coq.ZArith.Zbitwise]
Z.add_compare_mono_l [lemma, in Coq.ZArith.BinInt]
Z.add_diag [lemma, in Coq.ZArith.BinInt]
Z.add_reg_l [lemma, in Coq.ZArith.BinInt]
Z.add_succ_l [lemma, in Coq.ZArith.BinInt]
Z.add_0_l [lemma, in Coq.ZArith.BinInt]
Z.add_wd [definition, in Coq.ZArith.BinInt]
Z.add_lxor_2land [lemma, in Coq.ZArith.Zbitwise]
Z.add_lor_land [lemma, in Coq.ZArith.Zbitwise]
Z.add_lnot_r [lemma, in Coq.ZArith.Zbitwise]
Z.bi_induction [lemma, in Coq.ZArith.BinInt]
Z.compare [definition, in Coq.ZArith.BinIntDef]
Z.compare_opp [lemma, in Coq.ZArith.BinInt]
Z.compare_le_iff [lemma, in Coq.ZArith.BinInt]
Z.compare_lt_iff [lemma, in Coq.ZArith.BinInt]
Z.compare_antisym [lemma, in Coq.ZArith.BinInt]
Z.compare_sub [lemma, in Coq.ZArith.BinInt]
Z.compare_eq_iff [lemma, in Coq.ZArith.BinInt]
Z.Decidable_ge_Z [instance, in Coq.ZArith.BinInt]
Z.Decidable_gt_Z [instance, in Coq.ZArith.BinInt]
Z.Decidable_le_Z [instance, in Coq.ZArith.BinInt]
Z.Decidable_lt_Z [instance, in Coq.ZArith.BinInt]
Z.Decidable_eq_Z [instance, in Coq.ZArith.BinInt]
Z.div [definition, in Coq.ZArith.BinIntDef]
Z.divide [definition, in Coq.ZArith.BinInt]
Z.divide_Zpos_Zneg_l [lemma, in Coq.ZArith.BinInt]
Z.divide_Zpos_Zneg_r [lemma, in Coq.ZArith.BinInt]
Z.divide_Zpos [lemma, in Coq.ZArith.BinInt]
Z.divide_alt [lemma, in Coq.omega.PreOmega]
Z.div_eucl [definition, in Coq.ZArith.BinIntDef]
Z.div_mod [lemma, in Coq.ZArith.BinInt]
Z.div_eucl_eq [lemma, in Coq.ZArith.BinInt]
Z.div_wd [definition, in Coq.ZArith.BinInt]
Z.div_0_r_ext [lemma, in Coq.omega.PreOmega]
Z.div2 [definition, in Coq.ZArith.BinIntDef]
Z.div2_spec [lemma, in Coq.ZArith.BinInt]
Z.double [definition, in Coq.ZArith.BinIntDef]
Z.double_spec [lemma, in Coq.ZArith.BinInt]
Z.eq [definition, in Coq.ZArith.BinInt]
Z.eqb [definition, in Coq.ZArith.BinIntDef]
Z.eqb_eq [lemma, in Coq.ZArith.BinInt]
Z.eq_dec [definition, in Coq.ZArith.BinInt]
Z.eq_equiv [definition, in Coq.ZArith.BinInt]
Z.euclidean_division_equations_flags.DefaultHelpers [module, in Coq.omega.PreOmega]
Z.euclidean_division_equations_flags.find_duplicate_quotients [projection, in Coq.omega.PreOmega]
Z.euclidean_division_equations_flags.t [record, in Coq.omega.PreOmega]
Z.euclidean_division_equations_flags [module, in Coq.omega.PreOmega]
Z.even [definition, in Coq.ZArith.BinIntDef]
Z.Even [definition, in Coq.ZArith.BinInt]
Z.even_spec [lemma, in Coq.ZArith.BinInt]
Z.frexp [definition, in Coq.Floats.FloatOps]
Z.gcd [definition, in Coq.ZArith.BinIntDef]
Z.gcd_nonneg [lemma, in Coq.ZArith.BinInt]
Z.gcd_greatest [lemma, in Coq.ZArith.BinInt]
Z.gcd_divide_r [lemma, in Coq.ZArith.BinInt]
Z.gcd_divide_l [lemma, in Coq.ZArith.BinInt]
Z.ge [definition, in Coq.ZArith.BinInt]
Z.geb [definition, in Coq.ZArith.BinIntDef]
Z.geb_spec [lemma, in Coq.ZArith.BinInt]
Z.geb_le [lemma, in Coq.ZArith.BinInt]
Z.geb_leb [lemma, in Coq.ZArith.BinInt]
Z.geb_ge [lemma, in Coq.ZArith.BinInt]
Z.ge_le [lemma, in Coq.ZArith.BinInt]
Z.ge_le_iff [lemma, in Coq.ZArith.BinInt]
Z.ggcd [definition, in Coq.ZArith.BinIntDef]
Z.ggcd_opp [lemma, in Coq.ZArith.BinInt]
Z.ggcd_correct_divisors [lemma, in Coq.ZArith.BinInt]
Z.ggcd_gcd [lemma, in Coq.ZArith.BinInt]
Z.gt [definition, in Coq.ZArith.BinInt]
Z.gtb [definition, in Coq.ZArith.BinIntDef]
Z.gtb_spec [lemma, in Coq.ZArith.BinInt]
Z.gtb_lt [lemma, in Coq.ZArith.BinInt]
Z.gtb_ltb [lemma, in Coq.ZArith.BinInt]
Z.gtb_gt [lemma, in Coq.ZArith.BinInt]
Z.gt_lt [lemma, in Coq.ZArith.BinInt]
Z.gt_lt_iff [lemma, in Coq.ZArith.BinInt]
Z.iter [definition, in Coq.ZArith.BinIntDef]
Z.land [definition, in Coq.ZArith.BinIntDef]
Z.land_spec [lemma, in Coq.ZArith.BinInt]
Z.ldexp [definition, in Coq.Floats.FloatOps]
Z.ldiff [definition, in Coq.ZArith.BinIntDef]
Z.ldiff_spec [lemma, in Coq.ZArith.BinInt]
Z.ldiff_lor_land [lemma, in Coq.ZArith.Zbitwise]
Z.le [definition, in Coq.ZArith.BinInt]
Z.leb [definition, in Coq.ZArith.BinIntDef]
Z.leb_le [lemma, in Coq.ZArith.BinInt]
Z.le_ge [lemma, in Coq.ZArith.BinInt]
Z.lnot_sub [lemma, in Coq.ZArith.Zbitwise]
Z.lnot_opp [lemma, in Coq.ZArith.Zbitwise]
Z.lnot_eq_pred_opp [lemma, in Coq.ZArith.Zbitwise]
Z.lnot_pred [lemma, in Coq.ZArith.Zbitwise]
Z.lnot_lnot [lemma, in Coq.ZArith.Zbitwise]
Z.log2 [definition, in Coq.ZArith.BinIntDef]
Z.log2_nonpos [lemma, in Coq.ZArith.BinInt]
Z.log2_spec [lemma, in Coq.ZArith.BinInt]
Z.lor [definition, in Coq.ZArith.BinIntDef]
Z.lor_spec [lemma, in Coq.ZArith.BinInt]
Z.lt [definition, in Coq.ZArith.BinInt]
Z.ltb [definition, in Coq.ZArith.BinIntDef]
Z.ltb_lt [lemma, in Coq.ZArith.BinInt]
Z.lt_gt [lemma, in Coq.ZArith.BinInt]
Z.lt_succ_r [lemma, in Coq.ZArith.BinInt]
Z.lt_wd [definition, in Coq.ZArith.BinInt]
Z.lxor [definition, in Coq.ZArith.BinIntDef]
Z.lxor_spec [lemma, in Coq.ZArith.BinInt]
Z.max [definition, in Coq.ZArith.BinIntDef]
Z.max_r [lemma, in Coq.ZArith.BinInt]
Z.max_l [lemma, in Coq.ZArith.BinInt]
Z.min [definition, in Coq.ZArith.BinIntDef]
Z.min_r [lemma, in Coq.ZArith.BinInt]
Z.min_l [lemma, in Coq.ZArith.BinInt]
Z.modulo [definition, in Coq.ZArith.BinIntDef]
Z.mod_bound_pos_le [lemma, in Coq.ZArith.BinInt]
Z.mod_neg_bound [lemma, in Coq.ZArith.BinInt]
Z.mod_bound_pos [definition, in Coq.ZArith.BinInt]
Z.mod_pos_bound [lemma, in Coq.ZArith.BinInt]
Z.mod_wd [definition, in Coq.ZArith.BinInt]
Z.mod_0_r_ext [lemma, in Coq.omega.PreOmega]
Z.mul [definition, in Coq.ZArith.BinIntDef]
Z.mul_reg_r [lemma, in Coq.ZArith.BinInt]
Z.mul_reg_l [lemma, in Coq.ZArith.BinInt]
Z.mul_succ_l [lemma, in Coq.ZArith.BinInt]
Z.mul_0_l [lemma, in Coq.ZArith.BinInt]
Z.mul_wd [definition, in Coq.ZArith.BinInt]
Z.neg [abbreviation, in Coq.ZArith.BinIntDef]
Z.odd [definition, in Coq.ZArith.BinIntDef]
Z.Odd [definition, in Coq.ZArith.BinInt]
Z.odd_spec [lemma, in Coq.ZArith.BinInt]
Z.of_num_int [definition, in Coq.ZArith.BinIntDef]
Z.of_hex_int [definition, in Coq.ZArith.BinIntDef]
Z.of_int [definition, in Coq.ZArith.BinIntDef]
Z.of_num_uint [definition, in Coq.ZArith.BinIntDef]
Z.of_hex_uint [definition, in Coq.ZArith.BinIntDef]
Z.of_uint [definition, in Coq.ZArith.BinIntDef]
Z.of_N [definition, in Coq.ZArith.BinIntDef]
Z.of_nat [definition, in Coq.ZArith.BinIntDef]
Z.one [definition, in Coq.ZArith.BinIntDef]
Z.one_succ [lemma, in Coq.ZArith.BinInt]
Z.opp [definition, in Coq.ZArith.BinIntDef]
Z.opp_eq_mul_m1 [lemma, in Coq.ZArith.BinInt]
Z.opp_succ [lemma, in Coq.ZArith.BinInt]
Z.opp_0 [lemma, in Coq.ZArith.BinInt]
Z.opp_wd [definition, in Coq.ZArith.BinInt]
Z.opp_lnot [lemma, in Coq.ZArith.Zbitwise]
Z.peano_ind [lemma, in Coq.ZArith.BinInt]
Z.pos [abbreviation, in Coq.ZArith.BinIntDef]
Z.pos_div_eucl [definition, in Coq.ZArith.BinIntDef]
Z.pos_sub [definition, in Coq.ZArith.BinIntDef]
Z.pos_div_eucl_bound [lemma, in Coq.ZArith.BinInt]
Z.pos_div_eucl_eq [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_opp [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_gt [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_lt [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_diag [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_discr [lemma, in Coq.ZArith.BinInt]
Z.pos_sub_spec [lemma, in Coq.ZArith.BinInt]
Z.pow [definition, in Coq.ZArith.BinIntDef]
Z.pow_pos [definition, in Coq.ZArith.BinIntDef]
Z.pow_pos_fold [lemma, in Coq.ZArith.BinInt]
Z.pow_neg_r [lemma, in Coq.ZArith.BinInt]
Z.pow_succ_r [lemma, in Coq.ZArith.BinInt]
Z.pow_0_r [lemma, in Coq.ZArith.BinInt]
Z.pow_wd [definition, in Coq.ZArith.BinInt]
Z.pred [definition, in Coq.ZArith.BinIntDef]
Z.pred_double [definition, in Coq.ZArith.BinIntDef]
Z.pred_double_spec [lemma, in Coq.ZArith.BinInt]
Z.pred_succ [lemma, in Coq.ZArith.BinInt]
Z.pred_wd [definition, in Coq.ZArith.BinInt]
Z.pred_sub_lnot_r [lemma, in Coq.ZArith.Zbitwise]
Z.Private_BootStrap.mul_add_distr_r [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.mul_add_distr_pos [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.mul_opp_r [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.add_opp_diag_r [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.add_assoc [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.add_assoc_pos [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.pos_sub_add [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.opp_inj [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.opp_add_distr [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.add_comm [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.mul_1_l [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.mul_0_r [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap.add_0_r [lemma, in Coq.ZArith.BinInt]
Z.Private_BootStrap [module, in Coq.ZArith.BinInt]
Z.quot [definition, in Coq.ZArith.BinIntDef]
Z.quotrem [definition, in Coq.ZArith.BinIntDef]
Z.quotrem_eq [lemma, in Coq.ZArith.BinInt]
Z.quot_rem [lemma, in Coq.ZArith.BinInt]
Z.quot_rem' [lemma, in Coq.ZArith.BinInt]
Z.quot_wd [definition, in Coq.ZArith.BinInt]
Z.quot_0_r_ext [lemma, in Coq.omega.PreOmega]
Z.quot2 [definition, in Coq.ZArith.BinIntDef]
Z.rem [definition, in Coq.ZArith.BinIntDef]
Z.rem_opp_r [lemma, in Coq.ZArith.BinInt]
Z.rem_opp_l [lemma, in Coq.ZArith.BinInt]
Z.rem_opp_r' [lemma, in Coq.ZArith.BinInt]
Z.rem_opp_l' [lemma, in Coq.ZArith.BinInt]
Z.rem_bound_pos [lemma, in Coq.ZArith.BinInt]
Z.rem_wd [definition, in Coq.ZArith.BinInt]
Z.rem_bound_neg_neg [lemma, in Coq.omega.PreOmega]
Z.rem_bound_pos_neg [lemma, in Coq.omega.PreOmega]
Z.rem_bound_neg_pos [lemma, in Coq.omega.PreOmega]
Z.rem_bound_pos_pos [lemma, in Coq.omega.PreOmega]
Z.rem_0_r_ext [lemma, in Coq.omega.PreOmega]
Z.sgn [definition, in Coq.ZArith.BinIntDef]
Z.sgn_neg [lemma, in Coq.ZArith.BinInt]
Z.sgn_pos [lemma, in Coq.ZArith.BinInt]
Z.sgn_null [lemma, in Coq.ZArith.BinInt]
Z.shiftl [definition, in Coq.ZArith.BinIntDef]
Z.shiftl_spec_high [lemma, in Coq.ZArith.BinInt]
Z.shiftl_spec_low [lemma, in Coq.ZArith.BinInt]
Z.shiftr [definition, in Coq.ZArith.BinIntDef]
Z.shiftr_spec [lemma, in Coq.ZArith.BinInt]
Z.shiftr_spec_aux [lemma, in Coq.ZArith.BinInt]
Z.shiftr_addcarries_1 [lemma, in Coq.ZArith.Zbitwise]
Z.shiftr_adccarries_1 [lemma, in Coq.ZArith.Zbitwise]
Z.sqrt [definition, in Coq.ZArith.BinIntDef]
Z.sqrtrem [definition, in Coq.ZArith.BinIntDef]
Z.sqrtrem_sqrt [lemma, in Coq.ZArith.BinInt]
Z.sqrtrem_spec [lemma, in Coq.ZArith.BinInt]
Z.sqrt_neg [lemma, in Coq.ZArith.BinInt]
Z.sqrt_spec [lemma, in Coq.ZArith.BinInt]
Z.square [definition, in Coq.ZArith.BinIntDef]
Z.square_spec [lemma, in Coq.ZArith.BinInt]
Z.sub [definition, in Coq.ZArith.BinIntDef]
Z.sub_succ_r [lemma, in Coq.ZArith.BinInt]
Z.sub_0_r [lemma, in Coq.ZArith.BinInt]
Z.sub_wd [definition, in Coq.ZArith.BinInt]
Z.sub_2landn_lxor [lemma, in Coq.ZArith.Zbitwise]
Z.sub_lxor_2rlandn [lemma, in Coq.ZArith.Zbitwise]
Z.sub_2lor_lxor [lemma, in Coq.ZArith.Zbitwise]
Z.sub_land_same_l [lemma, in Coq.ZArith.Zbitwise]
Z.sub_landn_rlandn [lemma, in Coq.ZArith.Zbitwise]
Z.sub_lor_l_same_r [lemma, in Coq.ZArith.Zbitwise]
Z.sub_lor_l_same_l [lemma, in Coq.ZArith.Zbitwise]
Z.sub_lor_land [lemma, in Coq.ZArith.Zbitwise]
Z.sub_lnot_r [lemma, in Coq.ZArith.Zbitwise]
Z.succ [definition, in Coq.ZArith.BinIntDef]
Z.succ_double [definition, in Coq.ZArith.BinIntDef]
Z.succ_double_spec [lemma, in Coq.ZArith.BinInt]
Z.succ_pred [lemma, in Coq.ZArith.BinInt]
Z.succ_wd [definition, in Coq.ZArith.BinInt]
Z.succ_add_lnot_r [lemma, in Coq.ZArith.Zbitwise]
Z.succ_lnot [lemma, in Coq.ZArith.Zbitwise]
Z.t [definition, in Coq.ZArith.BinIntDef]
Z.testbit [definition, in Coq.ZArith.BinIntDef]
Z.testbit_ones_nonneg [lemma, in Coq.ZArith.BinInt]
Z.testbit_ones [lemma, in Coq.ZArith.BinInt]
Z.testbit_mod_pow2 [lemma, in Coq.ZArith.BinInt]
Z.testbit_even_succ [lemma, in Coq.ZArith.BinInt]
Z.testbit_odd_succ [lemma, in Coq.ZArith.BinInt]
Z.testbit_even_0 [lemma, in Coq.ZArith.BinInt]
Z.testbit_odd_0 [lemma, in Coq.ZArith.BinInt]
Z.testbit_neg_r [lemma, in Coq.ZArith.BinInt]
Z.testbit_0_l [lemma, in Coq.ZArith.BinInt]
Z.testbit_Zneg [lemma, in Coq.ZArith.BinInt]
Z.testbit_Zpos [lemma, in Coq.ZArith.BinInt]
Z.testbit_of_N' [lemma, in Coq.ZArith.BinInt]
Z.testbit_of_N [lemma, in Coq.ZArith.BinInt]
Z.testbit_wd [definition, in Coq.ZArith.BinInt]
Z.testbit_addcarries_pos [lemma, in Coq.ZArith.Zbitwise]
Z.testbit_addcarries_0 [lemma, in Coq.ZArith.Zbitwise]
Z.testbit_adccarries_pos [lemma, in Coq.ZArith.Zbitwise]
Z.testbit_adccarries_0 [lemma, in Coq.ZArith.Zbitwise]
Z.to_num_hex_int [definition, in Coq.ZArith.BinIntDef]
Z.to_num_int [definition, in Coq.ZArith.BinIntDef]
Z.to_hex_int [definition, in Coq.ZArith.BinIntDef]
Z.to_int [definition, in Coq.ZArith.BinIntDef]
Z.to_pos [definition, in Coq.ZArith.BinIntDef]
Z.to_N [definition, in Coq.ZArith.BinIntDef]
Z.to_nat [definition, in Coq.ZArith.BinIntDef]
Z.two [definition, in Coq.ZArith.BinIntDef]
Z.two_succ [lemma, in Coq.ZArith.BinInt]
Z.zero [definition, in Coq.ZArith.BinIntDef]
_ รท _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ mod _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ / _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ >? _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ >=? _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ <? _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ <=? _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ =? _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ ?= _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ ^ _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ * _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ - _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
- _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ + _ (Z_scope) [notation, in Coq.ZArith.BinIntDef]
_ < _ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ < _ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ > _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ >= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ < _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ <= _ (Z_scope) [notation, in Coq.ZArith.BinInt]
_ ^^ _ [notation, in Coq.ZArith.Zbitwise]
_ .[ _ ] [notation, in Coq.ZArith.Zbitwise]
_ .^ _ [notation, in Coq.ZArith.Zbitwise]
_ .& _ [notation, in Coq.ZArith.Zbitwise]
_ .| _ [notation, in Coq.ZArith.Zbitwise]
( _ | _ ) [notation, in Coq.ZArith.BinInt]
.~ _ [notation, in Coq.ZArith.Zbitwise]
Z0 [abbreviation, in Coq.ZArith.BinInt]
Z0 [constructor, in Coq.Numbers.BinNums]
Z2N [module, in Coq.ZArith.Znat]
Z2Nat [module, in Coq.ZArith.Znat]
Z2Nat.id [lemma, in Coq.ZArith.Znat]
Z2Nat.inj [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_pow [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_mod [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_div [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_max [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_min [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_lt [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_le [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_compare [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_pred [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_sub [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_succ [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_mul [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_add [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_neg [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_pos [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_0 [lemma, in Coq.ZArith.Znat]
Z2Nat.inj_iff [lemma, in Coq.ZArith.Znat]
Z2N.id [lemma, in Coq.ZArith.Znat]
Z2N.inj [lemma, in Coq.ZArith.Znat]
Z2N.inj_testbit [lemma, in Coq.ZArith.Znat]
Z2N.inj_pow [lemma, in Coq.ZArith.Znat]
Z2N.inj_quot2 [lemma, in Coq.ZArith.Znat]
Z2N.inj_div2 [lemma, in Coq.ZArith.Znat]
Z2N.inj_rem [lemma, in Coq.ZArith.Znat]
Z2N.inj_quot [lemma, in Coq.ZArith.Znat]
Z2N.inj_mod [lemma, in Coq.ZArith.Znat]
Z2N.inj_div [lemma, in Coq.ZArith.Znat]
Z2N.inj_max [lemma, in Coq.ZArith.Znat]
Z2N.inj_min [lemma, in Coq.ZArith.Znat]
Z2N.inj_lt [lemma, in Coq.ZArith.Znat]
Z2N.inj_le [lemma, in Coq.ZArith.Znat]
Z2N.inj_compare [lemma, in Coq.ZArith.Znat]
Z2N.inj_pred [lemma, in Coq.ZArith.Znat]
Z2N.inj_sub [lemma, in Coq.ZArith.Znat]
Z2N.inj_succ [lemma, in Coq.ZArith.Znat]
Z2N.inj_mul [lemma, in Coq.ZArith.Znat]
Z2N.inj_add [lemma, in Coq.ZArith.Znat]
Z2N.inj_neg [lemma, in Coq.ZArith.Znat]
Z2N.inj_pos [lemma, in Coq.ZArith.Znat]
Z2N.inj_0 [lemma, in Coq.ZArith.Znat]
Z2N.inj_iff [lemma, in Coq.ZArith.Znat]
Z2P [abbreviation, in Coq.QArith.Qreduction]
Z2Pos [module, in Coq.ZArith.BinInt]
Z2Pos.id [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_gcd [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_sqrt [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_min [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_max [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_eqb [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_ltb [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_leb [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_compare [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_pow_pos [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_pow [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_mul [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_pred [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_sub [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_add [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_succ [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_succ_double [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_double [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_1 [lemma, in Coq.ZArith.BinInt]
Z2Pos.inj_iff [lemma, in Coq.ZArith.BinInt]
Z2Pos.to_pos_nonpos [lemma, in Coq.ZArith.BinInt]
Z2P_correct [abbreviation, in Coq.QArith.Qreduction]


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 (25958 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 (999 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 (811 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 (1769 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 (587 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 (11879 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 (960 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 (508 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 (307 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 (479 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 (495 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 (905 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 (1199 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 (4894 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 (166 entries)