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 (19028 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 (451 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 (358 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 (101 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 (8297 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 (399 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 (754 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 (636 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 (404 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 (238 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 (3488 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 (612 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 (625 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 (2230 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 (435 entries)

Z

Z [module, in Coq.ZArith.Zminmax]
Z [inductive, in Coq.ZArith.BinInt]
Zabs [definition, in Coq.ZArith.BinInt]
Zabs [library]
Zabs_ind [lemma, in Coq.ZArith.Zabs]
Zabs_nat_Zsucc [lemma, in Coq.ZArith.Zabs]
Zabs_nat_lt [lemma, in Coq.ZArith.Zabs]
Zabs_Qabs [lemma, in Coq.QArith.Qabs]
Zabs_eq_case [lemma, in Coq.ZArith.Zabs]
Zabs_involutive [lemma, in Coq.ZArith.Zabs]
Zabs_Zsgn [lemma, in Coq.ZArith.Zabs]
Zabs_Zmult [lemma, in Coq.ZArith.Zabs]
Zabs_nat_Zminus [lemma, in Coq.ZArith.Zabs]
Zabs_triangle [lemma, in Coq.ZArith.Zabs]
Zabs_spec [lemma, in Coq.ZArith.Zabs]
Zabs_pos [lemma, in Coq.ZArith.Zabs]
Zabs_eq [lemma, in Coq.ZArith.Zabs]
Zabs_intro [lemma, in Coq.ZArith.Zabs]
Zabs_nat_Zplus [lemma, in Coq.ZArith.Zabs]
Zabs_nat [definition, in Coq.ZArith.BinInt]
Zabs_dec [definition, in Coq.ZArith.Zabs]
Zabs_square [lemma, in Coq.ZArith.Zabs]
Zabs_nat_mult [lemma, in Coq.ZArith.Zabs]
Zabs_nat_le [lemma, in Coq.ZArith.Zabs]
Zabs_non_eq [lemma, in Coq.ZArith.Zabs]
Zabs_Zopp [lemma, in Coq.ZArith.Zabs]
Zabs_N [definition, in Coq.ZArith.BinInt]
Zabs_nat_Z_of_nat [lemma, in Coq.ZArith.Zabs]
ZAdd [library]
ZAddOrder [library]
ZAddOrderPropFunct [module, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.add_nonpos_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.add_neg_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.add_neg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.add_nonpos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_sub_le_add_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_le_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_add_le_sub_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_sub_le_add [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_sub_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_sub_0 [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_0_sub [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_sub_le_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_add_le_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.le_lt_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_sub_lt_add [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_add_lt_sub_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_add_lt_sub_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_le_sub_lt [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_sub_0 [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_0_sub [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_sub_lt_add_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_sub_lt_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.lt_sub_pos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_nonpos_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_pos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_nonneg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.opp_neg_pos [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.PosNeg [section, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.PosNeg.P [variable, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.PosNeg.P_wd [variable, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_neg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_lt_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_nonpos [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_neg [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_nonneg [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_nonpos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_pos [abbreviation, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_lt_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_le_mono_r [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_le_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_le_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_lt_mono_l [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_lt_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_le_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.sub_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddOrderPropFunct.zero_pos_neg [lemma, in Coq.Numbers.Integer.Abstract.ZAddOrder]
ZAddPropFunct [module, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_add_simpl_r_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_sub_swap [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_simpl_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_move_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_add_simpl_l_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_simpl_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_opp_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_move_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_move_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_opp_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_add_simpl_r_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_add_simpl_l_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_move_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_sub_assoc [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.add_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.eq_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.eq_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_involutive [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_inj [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_inj_wd [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_add_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_pred [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.opp_sub_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_add_simpl_r_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_succ_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_add_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_simpl_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_add_simpl_r_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_move_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_move_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_simpl_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_move_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_sub_distr [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_diag [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZAddPropFunct.sub_move_0_r [lemma, in Coq.Numbers.Integer.Abstract.ZAdd]
ZArith [library]
ZArithProof [inductive, in Coq.micromega.ZMicromega]
ZArithRing [library]
ZArith_dec [library]
ZArith_base [library]
ZAxioms [library]
ZAxiomsExtSig [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZAxiomsExtSig' [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZAxiomsSig [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
ZAxiomsSig' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Zaxiom_one_zero [lemma, in Coq.nsatz.Nsatz]
ZBase [library]
ZBasePropFunct [module, in Coq.Numbers.Integer.Abstract.ZBase]
ZBasePropFunct.pred_inj_wd [lemma, in Coq.Numbers.Integer.Abstract.ZBase]
ZBasePropFunct.pred_inj [lemma, in Coq.Numbers.Integer.Abstract.ZBase]
ZBinary [library]
ZBinAxiomsMod [module, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.abs [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.abs_eq [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.abs_neq [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.add [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.add_succ_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.add_0_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.add_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.bi_induction [lemma, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.eq [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.eq_equiv [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.le [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.lt [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.lt_eq_cases [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.lt_succ_r [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.lt_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.lt_irrefl [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.max [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.max_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.max_r [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.min [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.min_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.min_r [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.mul [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.mul_0_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.mul_succ_l [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.mul_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.opp [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.opp_succ [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.opp_0 [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.opp_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.pred [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.pred_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.pred_succ [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sgn [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sgn_pos [lemma, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sgn_neg [lemma, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sgn_null [lemma, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sub [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sub_0_r [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sub_succ_r [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.sub_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.succ [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.succ_wd [instance, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.succ_pred [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.t [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinAxiomsMod.zero [definition, in Coq.Numbers.Integer.Binary.ZBinary]
ZBinPropMod [module, in Coq.Numbers.Integer.Binary.ZBinary]
Zbool [library]
Zbounded_induction [lemma, in Coq.Numbers.BigNumPrelude]
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 [definition, in Coq.ZArith.BinInt]
Zcompare [library]
ZcompareSpec [inductive, in Coq.Numbers.Cyclic.Int31.Cyclic31]
ZcompareSpecEq [constructor, in Coq.Numbers.Cyclic.Int31.Cyclic31]
ZcompareSpecGt [constructor, in Coq.Numbers.Cyclic.Int31.Cyclic31]
ZcompareSpecLt [constructor, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Zcompare_rect [lemma, in Coq.ZArith.ZArith_dec]
Zcompare_Gt_Lt_antisym [lemma, in Coq.ZArith.Zcompare]
Zcompare_Lt_trans [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_Gt [lemma, in Coq.ZArith.Zcompare]
Zcompare_antisym [lemma, in Coq.ZArith.Zcompare]
Zcompare_spec [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
Zcompare_eq_case [lemma, in Coq.ZArith.Zcompare]
Zcompare_spec [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_spec [lemma, in Coq.ZArith.Zcompare]
Zcompare_Eq_eq [lemma, in Coq.ZArith.Zcompare]
Zcompare_opp [lemma, in Coq.ZArith.Zcompare]
Zcompare_gt [lemma, in Coq.Numbers.BigNumPrelude]
Zcompare_rec [lemma, in Coq.ZArith.ZArith_dec]
Zcompare_mult_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_not_Lt [lemma, in Coq.ZArith.Zcompare]
Zcompare_succ_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_Eq_iff_eq [lemma, in Coq.ZArith.Zcompare]
Zcompare_plus_compat [lemma, in Coq.ZArith.Zcompare]
Zcompare_refl [lemma, in Coq.ZArith.Zcompare]
Zcompare_egal_dec [lemma, in Coq.ZArith.Zcompare]
Zcompare_elim [lemma, in Coq.ZArith.Zcompare]
Zcompare_Gt_trans [lemma, in Coq.ZArith.Zcompare]
Zcomplements [library]
ZC1 [lemma, in Coq.NArith.BinPos]
ZC2 [lemma, in Coq.NArith.BinPos]
ZC3 [lemma, in Coq.NArith.BinPos]
ZC4 [lemma, in Coq.NArith.BinPos]
ZDecAxiomsSig [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZDecAxiomsSig' [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
Zdi [instance, in Coq.nsatz.Nsatz]
Zdigits [library]
Zdiv [definition, in Coq.ZArith.Zdiv]
ZDiv [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDiv [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDiv [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
Zdiv [library]
ZDivEucl [library]
ZDivFloor [library]
Zdivide [inductive, in Coq.ZArith.Znumtheory]
Zdivide_minus_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zdiv_eq [lemma, in Coq.ZArith.Znumtheory]
Zdivide_le [lemma, in Coq.ZArith.Znumtheory]
Zdivide_antisym [lemma, in Coq.ZArith.Znumtheory]
Zdivide_pol_one [lemma, in Coq.micromega.ZMicromega]
Zdivide_Zdiv_eq_2 [lemma, in Coq.ZArith.Znumtheory]
Zdivide_dec [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zabs_inv_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_factor_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zdiv_lt_pos [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_pol [inductive, in Coq.micromega.ZMicromega]
Zdivide_mod_minus [lemma, in Coq.ZArith.Znumtheory]
Zdivide_refl [lemma, in Coq.ZArith.Znumtheory]
Zdivide_power_2 [lemma, in Coq.ZArith.Zpow_facts]
Zdivide_0 [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zabs_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_intro [constructor, in Coq.ZArith.Znumtheory]
Zdivide_plus_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mult_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_factor_r [lemma, in Coq.ZArith.Znumtheory]
Zdivide_Zgcd [lemma, in Coq.ZArith.Znumtheory]
Zdivide_pol_sub_0 [lemma, in Coq.micromega.ZMicromega]
Zdivide_pol_sub [lemma, in Coq.micromega.ZMicromega]
Zdivide_opp_l_rev [lemma, in Coq.ZArith.Znumtheory]
Zdivide_mult_l [lemma, in Coq.ZArith.Znumtheory]
Zdivide_bounds [lemma, in Coq.ZArith.Znumtheory]
Zdivide_pol_Zdivide [lemma, in Coq.micromega.ZMicromega]
Zdivide_mod [lemma, in Coq.ZArith.Znumtheory]
Zdivide_1 [lemma, in Coq.ZArith.Znumtheory]
Zdivide_trans [lemma, in Coq.ZArith.Znumtheory]
Zdivide_opp_r_rev [lemma, in Coq.ZArith.Znumtheory]
ZDivPropFunct [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.add_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.add_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.add_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.add_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.add_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.add_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.add_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.add_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.add_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_opp_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_opp_r_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_unique_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_unique_neg [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_mul_cancel_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_add_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_le_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_exact [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_mul_cancel_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_opp_r_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_lt_upper_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_div [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_mul_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_opp_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_le_lower_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_le_compat_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.div_str_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.div_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.div_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_sign [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_sign [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_opp_opp_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_1_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_opp_l_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_bound_or [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_1_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_opp_r_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_opp_opp_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_0_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_same [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_opp_l_nz [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_add [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_unique_neg [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_divides [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_unique_pos [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_mul [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_divides [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_small_iff [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_unique [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mod_eq [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_small [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_opp_r_z [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mod_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mod_divides [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_succ_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_div_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_succ_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_pred_div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_succ_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_pred_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_mod_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_mod [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_succ_div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_div_ge [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_div_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.mul_pred_div_gt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_div_ge [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_succ_div_lt [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.mul_mod_idemp_r [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_div_le [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.mul_mod_idemp_l [lemma, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.NZDivP [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.NZDivP [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.NZDivP [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivPropFunct.opp_mod_bound_or [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.div [definition, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.div [definition, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD.div_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD.div_mod [definition, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.div_mod [definition, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD.div_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.modulo [definition, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD.modulo [definition, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.mod_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.mod_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivPropFunct.ZD.mod_bound [lemma, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivPropFunct.ZD.mod_wd [definition, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivSig [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivSig [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSig [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSig' [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivSig' [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSig' [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSpecific [module, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivSpecific [module, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSpecific [module, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSpecific.mod_bound [axiom, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSpecific.mod_opp_l [axiom, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSpecific.mod_neg_bound [axiom, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSpecific.mod_opp_r [axiom, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
ZDivSpecific.mod_pos_bound [axiom, in Coq.Numbers.Integer.Abstract.ZDivFloor]
ZDivSpecific.mod_always_pos [axiom, in Coq.Numbers.Integer.Abstract.ZDivEucl]
ZDivTrunc [library]
Zdiv_rest_correct2 [lemma, in Coq.ZArith.Zpower]
Zdiv_0_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_Zdiv [lemma, in Coq.ZArith.Zdiv]
Zdiv_le_upper_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_rest_correct1 [lemma, in Coq.ZArith.Zpower]
Zdiv_neg [lemma, in Coq.Numbers.BigNumPrelude]
Zdiv_eucl_exist [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_cancel_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_opp_opp [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_cancel_l [definition, in Coq.Numbers.BigNumPrelude]
Zdiv_rest_aux [definition, in Coq.ZArith.Zpower]
Zdiv_1_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_unique_full [lemma, in Coq.ZArith.Zdiv]
Zdiv_mod_unique [lemma, in Coq.ZArith.Zdiv]
Zdiv_shift_r [lemma, in Coq.Numbers.BigNumPrelude]
Zdiv_mult_le [lemma, in Coq.ZArith.Zdiv]
Zdiv_le_compat_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_gcd_zero [lemma, in Coq.Numbers.BigNumPrelude]
Zdiv_rest_correct [lemma, in Coq.ZArith.Zpower]
Zdiv_unique [lemma, in Coq.ZArith.Zdiv]
Zdiv_Pinj [constructor, in Coq.micromega.ZMicromega]
Zdiv_pol [definition, in Coq.micromega.ZMicromega]
Zdiv_1_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_sgn [lemma, in Coq.ZArith.Zdiv]
Zdiv_0_l [lemma, in Coq.ZArith.Zdiv]
Zdiv_rest [definition, in Coq.ZArith.Zpower]
Zdiv_mod_unique_2 [lemma, in Coq.ZArith.Zdiv]
Zdiv_PX [constructor, in Coq.micromega.ZMicromega]
Zdiv_le_lower_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_pol_correct [lemma, in Coq.micromega.ZMicromega]
Zdiv_Pc [constructor, in Coq.micromega.ZMicromega]
Zdiv_eucl_extended [lemma, in Coq.ZArith.Zdiv]
Zdiv_small [lemma, in Coq.ZArith.Zdiv]
Zdiv_rest_proof [constructor, in Coq.ZArith.Zpower]
Zdiv_mult_cancel_r [lemma, in Coq.ZArith.Zdiv]
Zdiv_mult_cancel_r [definition, in Coq.Numbers.BigNumPrelude]
Zdiv_lt_upper_bound [lemma, in Coq.ZArith.Zdiv]
Zdiv_eucl_POS [definition, in Coq.ZArith.Zdiv]
Zdiv_rest_proofs [inductive, in Coq.ZArith.Zpower]
Zdiv_eucl [definition, in Coq.ZArith.Zdiv]
Zdiv2 [definition, in Coq.ZArith.Zeven]
Zdiv2_two_power_nat [lemma, in Coq.ZArith.Zdigits]
Zdouble [definition, in Coq.ZArith.BinInt]
Zdouble_plus_one [definition, in Coq.ZArith.BinInt]
Zdouble_minus_one [definition, in Coq.ZArith.BinInt]
Zdouble_mult [lemma, in Coq.ZArith.BinInt]
Zdouble_plus_one_mult [lemma, in Coq.ZArith.BinInt]
Zegal_left [lemma, in Coq.ZArith.auxiliary]
zenon_notequiv_s [definition, in Coq.dp.Dp]
zenon_or_s [definition, in Coq.dp.Dp]
zenon_ex_s [definition, in Coq.dp.Dp]
zenon_equal_step [lemma, in Coq.dp.Dp]
zenon_imply_s [definition, in Coq.dp.Dp]
zenon_and [lemma, in Coq.dp.Dp]
zenon_pnotp_s [definition, in Coq.dp.Dp]
zenon_notand_s [definition, in Coq.dp.Dp]
zenon_notequiv [lemma, in Coq.dp.Dp]
zenon_equal_base [lemma, in Coq.dp.Dp]
zenon_imply [lemma, in Coq.dp.Dp]
zenon_notex [lemma, in Coq.dp.Dp]
zenon_nottrue [lemma, in Coq.dp.Dp]
zenon_notor [lemma, in Coq.dp.Dp]
zenon_notimply [lemma, in Coq.dp.Dp]
zenon_notall_s [definition, in Coq.dp.Dp]
zenon_notimply_s [definition, in Coq.dp.Dp]
zenon_and_s [definition, in Coq.dp.Dp]
zenon_equiv [lemma, in Coq.dp.Dp]
zenon_notand [lemma, in Coq.dp.Dp]
zenon_noteq [lemma, in Coq.dp.Dp]
zenon_equiv_s [definition, in Coq.dp.Dp]
zenon_notor_s [definition, in Coq.dp.Dp]
zenon_notequal [lemma, in Coq.dp.Dp]
zenon_notall [lemma, in Coq.dp.Dp]
zenon_or [lemma, in Coq.dp.Dp]
zenon_notequal_s [definition, in Coq.dp.Dp]
zenon_pnotp [lemma, in Coq.dp.Dp]
zenon_all [lemma, in Coq.dp.Dp]
zenon_ex [lemma, in Coq.dp.Dp]
Zeq [definition, in Coq.ring.LegacyZArithRing]
Zeqe [lemma, in Coq.setoid_ring.InitialRing]
Zeq_le [lemma, in Coq.ZArith.Zorder]
Zeq_bool_if [lemma, in Coq.ZArith.Zbool]
Zeq_bool [definition, in Coq.ZArith.Zbool]
Zeq_plus_swap [lemma, in Coq.ZArith.Zorder]
Zeq_bool_neq [lemma, in Coq.ZArith.Zbool]
Zeq_minus [lemma, in Coq.ZArith.BinInt]
Zeq_is_eq_bool [lemma, in Coq.ZArith.Zbool]
Zeq_prop [lemma, in Coq.ring.LegacyZArithRing]
Zeq_bool_eq [lemma, in Coq.ZArith.Zbool]
Zeq_bool_complete [lemma, in Coq.setoid_ring.RealField]
zero [projection, in Coq.nsatz.Nsatz]
zero [definition, in Coq.Strings.Ascii]
Zero [record, in Coq.nsatz.Nsatz]
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_intro [lemma, in Coq.Bool.Zerob]
zerob_true_elim [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]
1 [notation, in Coq.Numbers.NatInt.NZAxioms]
2 [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_ring [instance, in Coq.nsatz.Nsatz]
ZERO_le_N_digits [lemma, in Coq.ZArith.Zlogarithm]
Zeval_nformula_dec [lemma, in Coq.micromega.ZMicromega]
Zeval_expr [definition, in Coq.micromega.ZMicromega]
Zeval_expr_compat [lemma, in Coq.micromega.ZMicromega]
Zeval_formula [definition, in Coq.micromega.ZMicromega]
Zeval_formula' [definition, in Coq.micromega.ZMicromega]
Zeval_formula_compat [lemma, in Coq.micromega.ZMicromega]
Zeval_op2 [definition, in Coq.micromega.ZMicromega]
Zeval_op1 [definition, in Coq.micromega.ZMicromega]
Zeven [definition, in Coq.ZArith.Zeven]
Zeven [library]
Zeven_pred [lemma, in Coq.ZArith.Zeven]
Zeven_bool [definition, in Coq.ZArith.Zeven]
Zeven_mult_Zeven_l [lemma, in Coq.ZArith.Zeven]
Zeven_ex [lemma, in Coq.ZArith.Zeven]
Zeven_Sn [lemma, in Coq.ZArith.Zeven]
Zeven_2p [lemma, in Coq.ZArith.Zeven]
Zeven_div2 [lemma, in Coq.ZArith.Zeven]
Zeven_not_Zodd [lemma, in Coq.ZArith.Zeven]
Zeven_odd_bool [definition, in Coq.ZArith.Zbool]
Zeven_dec [definition, in Coq.ZArith.Zeven]
Zeven_bit_value [lemma, in Coq.ZArith.Zdigits]
Zeven_plus_Zeven [lemma, in Coq.ZArith.Zeven]
Zeven_plus_Zodd [lemma, in Coq.ZArith.Zeven]
Zeven_mult_Zeven_r [lemma, in Coq.ZArith.Zeven]
Zeven_odd_dec [definition, in Coq.ZArith.Zeven]
Zgcd [definition, in Coq.ZArith.Znumtheory]
ZgcdM [definition, in Coq.micromega.ZMicromega]
Zgcdn [definition, 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]
Zgcdn_ok_before_fibonacci [lemma, in Coq.ZArith.Zgcd_alt]
Zgcdn_is_gcd [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_mult_rel_prime [lemma, in Coq.Numbers.BigNumPrelude]
Zgcd_bound [definition, in Coq.ZArith.Zgcd_alt]
Zgcd_alt [definition, in Coq.ZArith.Zgcd_alt]
Zgcd_alt_pos [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_Zabs [lemma, in Coq.ZArith.Znumtheory]
Zgcd_bound_fibonacci [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_is_gcd [lemma, in Coq.ZArith.Znumtheory]
Zgcd_ass [lemma, in Coq.ZArith.Znumtheory]
Zgcd_div_pos [lemma, in Coq.Numbers.BigNumPrelude]
Zgcd_pol_correct_lt [lemma, in Coq.micromega.ZMicromega]
Zgcd_div_swap0 [lemma, in Coq.ZArith.Znumtheory]
Zgcd_pol_div [lemma, in Coq.micromega.ZMicromega]
Zgcd_div_swap [lemma, in Coq.ZArith.Znumtheory]
Zgcd_1_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Zgcd_pol_ge [lemma, in Coq.micromega.ZMicromega]
Zgcd_inv_0_r [lemma, in Coq.ZArith.Znumtheory]
Zgcd_is_pos [lemma, in Coq.ZArith.Znumtheory]
Zgcd_minus [lemma, in Coq.micromega.ZMicromega]
Zgcd_spec [lemma, in Coq.ZArith.Znumtheory]
Zgcd_comm [lemma, in Coq.ZArith.Znumtheory]
Zgcd_inv_0_l [lemma, in Coq.ZArith.Znumtheory]
Zgcd_1 [lemma, in Coq.ZArith.Znumtheory]
Zgcd_pol [definition, in Coq.micromega.ZMicromega]
Zgcd_is_gcd [lemma, in Coq.ZArith.Zgcd_alt]
Zgcd_bound [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zgcd_0 [lemma, in Coq.ZArith.Znumtheory]
Zgcd_alt [library]
Zge [definition, in Coq.ZArith.BinInt]
Zge_trans [lemma, in Coq.ZArith.Zorder]
Zge_minus_two_power_nat_S [lemma, in Coq.ZArith.Zdigits]
Zge_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zge_iff_le [lemma, in Coq.ZArith.Zorder]
Zge_left [lemma, in Coq.ZArith.auxiliary]
Zge_compare [lemma, in Coq.ZArith.Zcompare]
Zge_le [lemma, in Coq.ZArith.Zorder]
Zge_cases [lemma, in Coq.ZArith.Zbool]
Zge_bool [definition, in Coq.ZArith.Zbool]
Zggcd [definition, in Coq.ZArith.Znumtheory]
Zggcd_gcd [lemma, in Coq.ZArith.Znumtheory]
Zggcd_opp [lemma, in Coq.ZArith.Znumtheory]
Zggcd_correct_divisors [lemma, in Coq.ZArith.Znumtheory]
Zgt [definition, in Coq.ZArith.BinInt]
Zgt_iff_lt [lemma, in Coq.ZArith.Zorder]
Zgt_pos_0 [lemma, in Coq.ZArith.Zorder]
Zgt_irrefl [lemma, in Coq.ZArith.Zorder]
Zgt_left [lemma, in Coq.ZArith.auxiliary]
Zgt_trans_succ [lemma, in Coq.ZArith.Zorder]
Zgt_asym [lemma, in Coq.ZArith.Zorder]
Zgt_lt [lemma, in Coq.ZArith.Zorder]
Zgt_succ_le [lemma, in Coq.ZArith.Zorder]
Zgt_cases [lemma, in Coq.ZArith.Zbool]
Zgt_succ [lemma, in Coq.ZArith.Zorder]
Zgt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zgt_bool [definition, in Coq.ZArith.Zbool]
Zgt_is_gt_bool [lemma, in Coq.ZArith.Zbool]
Zgt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zgt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zgt_le_succ [lemma, in Coq.ZArith.Zorder]
Zgt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zgt_left_gt [lemma, in Coq.ZArith.auxiliary]
Zgt_le_trans [lemma, in Coq.ZArith.Zorder]
Zgt_compare [lemma, in Coq.ZArith.Zcompare]
Zgt_succ_gt_or_eq [lemma, in Coq.ZArith.Zorder]
Zgt_not_le [lemma, in Coq.ZArith.Zorder]
Zgt_trans [lemma, in Coq.ZArith.Zorder]
Zgt_succ_pred [lemma, in Coq.ZArith.Zorder]
ZHasMinMax [module, in Coq.ZArith.Zminmax]
ZHasMinMax.max [definition, in Coq.ZArith.Zminmax]
ZHasMinMax.max_r [definition, in Coq.ZArith.Zminmax]
ZHasMinMax.max_l [definition, in Coq.ZArith.Zminmax]
ZHasMinMax.min [definition, in Coq.ZArith.Zminmax]
ZHasMinMax.min_r [definition, in Coq.ZArith.Zminmax]
ZHasMinMax.min_l [definition, in Coq.ZArith.Zminmax]
Zhints [library]
Zind [lemma, in Coq.ZArith.BinInt]
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_1 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_minus [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_uniqueness_apart_sign [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_intro [constructor, in Coq.ZArith.Znumtheory]
Zis_gcd_refl [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid2 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_gcd [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd [inductive, in Coq.ZArith.Znumtheory]
Zis_gcd_unique [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_mod [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
Zis_gcd_0_abs [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_even_odd [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_rel_prime [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_sym [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_0 [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_for_euclid [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_bezout [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_opp [lemma, in Coq.ZArith.Znumtheory]
Zis_gcd_mult [lemma, in Coq.ZArith.Znumtheory]
Zle [definition, in Coq.ZArith.BinInt]
Zlength [definition, in Coq.ZArith.Zcomplements]
Zlength_correct [lemma, in Coq.ZArith.Zcomplements]
Zlength_cons [lemma, in Coq.ZArith.Zcomplements]
Zlength_aux [definition, in Coq.ZArith.Zcomplements]
Zlength_nil_inv [lemma, in Coq.ZArith.Zcomplements]
Zlength_properties.A [variable, in Coq.ZArith.Zcomplements]
Zlength_nil [lemma, in Coq.ZArith.Zcomplements]
Zlength_properties [section, in Coq.ZArith.Zcomplements]
Zle_max_l [definition, in Coq.ZArith.Zmax]
Zle_min_l [definition, in Coq.ZArith.Zmin]
Zle_plus_swap [lemma, in Coq.ZArith.Zorder]
Zle_bool [definition, in Coq.ZArith.Zbool]
Zle_antisym [lemma, in Coq.ZArith.Zorder]
Zle_0_nat [lemma, in Coq.ZArith.Zorder]
Zle_cases [lemma, in Coq.ZArith.Zbool]
Zle_pred [lemma, in Coq.ZArith.Zorder]
Zle_neg_pos [lemma, in Coq.ZArith.Zorder]
Zle_lt_or_eq_iff [lemma, in Coq.ZArith.Zorder]
Zle_gt_trans [lemma, in Coq.ZArith.Zorder]
Zle_minus_le_0 [lemma, in Coq.ZArith.Zorder]
Zle_not_gt [lemma, in Coq.ZArith.Zorder]
Zle_max_r [definition, in Coq.ZArith.Zmax]
Zle_le_succ [lemma, in Coq.ZArith.Zorder]
Zle_bool_plus_mono [lemma, in Coq.ZArith.Zbool]
Zle_not_lt [lemma, in Coq.ZArith.Zorder]
Zle_succ_gt [lemma, in Coq.ZArith.Zorder]
Zle_min_r [definition, in Coq.ZArith.Zmin]
Zle_gt_succ [lemma, in Coq.ZArith.Zorder]
Zle_0_minus_le [lemma, in Coq.ZArith.Zorder]
Zle_succ_le [lemma, in Coq.ZArith.Zorder]
Zle_mult_approx [lemma, in Coq.ZArith.auxiliary]
Zle_lt_trans [lemma, in Coq.ZArith.Zorder]
Zle_refl [lemma, in Coq.ZArith.Zorder]
Zle_left [lemma, in Coq.ZArith.auxiliary]
Zle_bool_refl [lemma, in Coq.ZArith.Zbool]
Zle_ge [lemma, in Coq.ZArith.Zorder]
Zle_or_lt [lemma, in Coq.ZArith.Zorder]
Zle_min_compat_r [definition, in Coq.ZArith.Zmin]
Zle_bool_imp_le [lemma, in Coq.ZArith.Zbool]
Zle_lt_succ [lemma, in Coq.ZArith.Zorder]
Zle_bool_trans [lemma, in Coq.ZArith.Zbool]
Zle_compare [lemma, in Coq.ZArith.Zcompare]
Zle_left_rev [lemma, in Coq.ZArith.auxiliary]
Zle_trans [lemma, in Coq.ZArith.Zorder]
Zle_min_compat_l [definition, in Coq.ZArith.Zmin]
Zle_0_1 [lemma, in Coq.ZArith.Zorder]
Zle_max_compat_r [definition, in Coq.ZArith.Zmax]
Zle_succ [lemma, in Coq.ZArith.Zorder]
Zle_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_bool_total [definition, in Coq.ZArith.Zbool]
Zle_max_compat_l [definition, in Coq.ZArith.Zmax]
Zle_lt_or_eq [lemma, in Coq.ZArith.Zorder]
Zle_0_pos [lemma, in Coq.ZArith.Zorder]
Zle_imp_le_bool [lemma, in Coq.ZArith.Zbool]
Zle_bool_antisym [lemma, in Coq.ZArith.Zbool]
Zlogarithm [library]
Zlt [definition, in Coq.ZArith.BinInt]
ZLt [library]
Zlt_succ [lemma, in Coq.ZArith.Zorder]
Zlt_lower_bound_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_compare [lemma, in Coq.ZArith.Zcompare]
Zlt_neg_0 [lemma, in Coq.ZArith.Zorder]
Zlt_two_power_nat_S [lemma, in Coq.ZArith.Zdigits]
Zlt_0_1 [lemma, in Coq.ZArith.Zorder]
Zlt_lt_double [lemma, in Coq.ZArith.Zpower]
Zlt_cotrans_pos [lemma, in Coq.ZArith.ZArith_dec]
Zlt_irrefl [lemma, in Coq.ZArith.Zorder]
Zlt_not_eq [lemma, in Coq.ZArith.Zorder]
Zlt_le_trans [lemma, in Coq.ZArith.Zorder]
Zlt_pred [lemma, in Coq.ZArith.Zorder]
Zlt_plus_swap [lemma, in Coq.ZArith.Zorder]
Zlt_lower_bound_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_trans [lemma, in Coq.ZArith.Zorder]
Zlt_left_lt [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 [lemma, in Coq.ZArith.Zorder]
Zlt_0_le_0_pred [lemma, in Coq.ZArith.Zorder]
Zlt_succ_pred [lemma, in Coq.ZArith.Zorder]
Zlt_square_simpl [lemma, in Coq.ZArith.Zorder]
Zlt_le_succ [lemma, in Coq.ZArith.Zorder]
Zlt_gt [lemma, in Coq.ZArith.Zorder]
Zlt_cotrans_neg [lemma, in Coq.ZArith.ZArith_dec]
Zlt_is_lt_bool [lemma, in Coq.ZArith.Zbool]
Zlt_succ_le [lemma, in Coq.ZArith.Zorder]
Zlt_asym [lemma, in Coq.ZArith.Zorder]
Zlt_is_le_bool [lemma, in Coq.ZArith.Zbool]
Zlt_0_rec [lemma, in Coq.ZArith.Wf_Z]
Zlt_succ_r [lemma, in Coq.ZArith.Zorder]
Zlt_left [lemma, in Coq.ZArith.auxiliary]
Zlt_not_le [lemma, in Coq.ZArith.Zorder]
Zlt_le_weak [lemma, in Coq.ZArith.Zorder]
Zlt_bool [definition, in Coq.ZArith.Zbool]
Zlt_0_ind [lemma, in Coq.ZArith.Wf_Z]
Zlt_cotrans [lemma, in Coq.ZArith.ZArith_dec]
Zlt_lt_succ [lemma, in Coq.ZArith.Zorder]
Zlt_cases [lemma, in Coq.ZArith.Zbool]
Zlt_left_rev [lemma, in Coq.ZArith.auxiliary]
Zlt0_not_eq [lemma, in Coq.Numbers.BigNumPrelude]
ZL0 [lemma, in Coq.ZArith.BinInt]
ZL10 [lemma, in Coq.NArith.BinPos]
ZL11 [lemma, in Coq.NArith.BinPos]
ZL16 [lemma, in Coq.NArith.Pnat]
ZL17 [lemma, in Coq.NArith.Pnat]
ZL3 [lemma, in Coq.NArith.Pnat]
ZL4 [lemma, in Coq.NArith.Pnat]
ZL4_inf [lemma, in Coq.ZArith.Wf_Z]
ZL5 [lemma, in Coq.NArith.Pnat]
ZL6 [lemma, in Coq.NArith.Pnat]
ZL7 [lemma, in Coq.NArith.Pnat]
ZL8 [lemma, in Coq.NArith.Pnat]
ZMake [library]
Zmax [definition, in Coq.ZArith.Zminmax]
Zmax [library]
Zmax_case [definition, in Coq.ZArith.Zmax]
Zmax_idempotent [definition, in Coq.ZArith.Zmax]
Zmax_spec [lemma, in Coq.ZArith.Zmax]
Zmax_irreducible_dec [lemma, in Coq.ZArith.Zmax]
Zmax_r [lemma, in Coq.ZArith.Zminmax]
Zmax_comm [definition, in Coq.ZArith.Zmax]
Zmax_irreducible_inf [abbreviation, in Coq.ZArith.Zmax]
Zmax_lub [definition, in Coq.ZArith.Zmax]
Zmax_min_absorption_r_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax_le_prime [definition, in Coq.ZArith.Zmax]
Zmax_case_strong [definition, in Coq.ZArith.Zmax]
Zmax_l [lemma, in Coq.ZArith.Zminmax]
Zmax_assoc [definition, in Coq.ZArith.Zmax]
Zmax_le_prime_inf [abbreviation, in Coq.ZArith.Zmax]
Zmax_min_modular_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax_right [definition, in Coq.ZArith.Zmax]
Zmax_left [lemma, in Coq.ZArith.Zmax]
Zmax_lub_lt [definition, in Coq.ZArith.Zmax]
Zmax_min_distr_r [abbreviation, in Coq.ZArith.Zminmax]
Zmax1 [abbreviation, in Coq.ZArith.Zmax]
Zmax2 [abbreviation, in Coq.ZArith.Zmax]
ZMicromega [library]
Zmin [definition, in Coq.ZArith.Zminmax]
Zmin [library]
Zminmax [library]
Zminus [definition, in Coq.ZArith.BinInt]
Zminus_succ_l [lemma, in Coq.ZArith.BinInt]
Zminus_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zminus_0_r [lemma, in Coq.ZArith.BinInt]
Zminus_mod [lemma, in Coq.ZArith.Zdiv]
Zminus_plus [lemma, in Coq.ZArith.BinInt]
Zminus_plus_simpl_r [lemma, in Coq.ZArith.BinInt]
Zminus_diag [lemma, in Coq.ZArith.BinInt]
Zminus_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zminus_eq [lemma, in Coq.ZArith.BinInt]
Zminus_0_l_reverse [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_plus_distr [lemma, in Coq.ZArith.BinInt]
Zminus_succ_r [lemma, in Coq.ZArith.BinInt]
Zminus_diag_reverse [lemma, in Coq.ZArith.BinInt]
Zmin_plus [abbreviation, in Coq.ZArith.Zmin]
Zmin_max_absorption_r_r [abbreviation, in Coq.ZArith.Zminmax]
Zmin_irreducible [lemma, in Coq.ZArith.Zmin]
Zmin_glb_lt [definition, in Coq.ZArith.Zmin]
Zmin_assoc [definition, in Coq.ZArith.Zmin]
Zmin_SS [abbreviation, in Coq.ZArith.Zmin]
Zmin_max_modular_r [abbreviation, in Coq.ZArith.Zminmax]
Zmin_idempotent [definition, in Coq.ZArith.Zmin]
Zmin_l [lemma, in Coq.ZArith.Zminmax]
Zmin_case [definition, in Coq.ZArith.Zmin]
Zmin_le_prime_inf [lemma, in Coq.ZArith.Zmin]
Zmin_spec [lemma, in Coq.ZArith.Zmin]
Zmin_r [lemma, in Coq.ZArith.Zminmax]
Zmin_glb [definition, in Coq.ZArith.Zmin]
Zmin_or [abbreviation, in Coq.ZArith.Zmin]
Zmin_max_distr_r [abbreviation, in Coq.ZArith.Zminmax]
Zmin_case_strong [definition, in Coq.ZArith.Zmin]
Zmin_n_n [abbreviation, in Coq.ZArith.Zmin]
Zmin_irreducible_inf [lemma, in Coq.ZArith.Zmin]
Zmin_comm [definition, in Coq.ZArith.Zmin]
Zmisc [library]
Zmod [definition, in Coq.ZArith.Zdiv]
ZModulo [section, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModulo [library]
ZModuloCyclicType [module, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModuloCyclicType.w [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModuloCyclicType.w_spec [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModuloCyclicType.w_op [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModulo.digits [variable, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModulo.digits_gt_1 [variable, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
ZModulo.digits_ne_1 [variable, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
[+| _ |] [notation, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
[-| _ |] [notation, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
[| _ |] [notation, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
[|| _ ||] [notation, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zmod_le [lemma, in Coq.ZArith.Zdiv]
Zmod_0_r [lemma, in Coq.ZArith.Zdiv]
Zmod_eq_full [lemma, in Coq.ZArith.Zdiv]
Zmod_divide [lemma, in Coq.ZArith.Znumtheory]
Zmod_mod [lemma, in Coq.ZArith.Zdiv]
Zmod_unique_full [lemma, in Coq.ZArith.Zdiv]
Zmod_POS_correct [lemma, in Coq.ZArith.Zdiv]
Zmod_0_l [lemma, in Coq.ZArith.Zdiv]
Zmod_div_mod [lemma, in Coq.ZArith.Znumtheory]
Zmod_1_r [lemma, in Coq.ZArith.Zdiv]
Zmod_divides [lemma, in Coq.ZArith.Zdiv]
Zmod_shift_r [lemma, in Coq.Numbers.BigNumPrelude]
Zmod_unique [lemma, in Coq.ZArith.Zdiv]
Zmod_distr [lemma, in Coq.Numbers.BigNumPrelude]
Zmod_1_l [lemma, in Coq.ZArith.Zdiv]
zmod_spec [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zmod_eqm [lemma, in Coq.ZArith.Zdiv]
Zmod_divide_minus [lemma, in Coq.ZArith.Znumtheory]
Zmod_eq [lemma, in Coq.ZArith.Zdiv]
Zmod_opp_opp [lemma, in Coq.ZArith.Zdiv]
Zmod_le_first [lemma, in Coq.Numbers.BigNumPrelude]
Zmod_equal [lemma, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zmod_small [lemma, in Coq.ZArith.Zdiv]
Zmod_POS [definition, in Coq.ZArith.Zdiv]
zmod_op [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Zmod' [definition, in Coq.ZArith.Zdiv]
Zmod'_correct [lemma, in Coq.ZArith.Zdiv]
Zmod2 [definition, in Coq.ZArith.Zdigits]
Zmod2_twice [lemma, in Coq.ZArith.Zdigits]
zmon [constructor, in Coq.micromega.EnvRing]
zmon [constructor, in Coq.setoid_ring.Ring_polynom]
zmon_pred [definition, in Coq.setoid_ring.Ring_polynom]
zmon_pred [definition, in Coq.micromega.EnvRing]
zmon_pred_ok [lemma, in Coq.setoid_ring.Ring_polynom]
zmon_pred_ok [lemma, in Coq.micromega.EnvRing]
ZMORPHISM [section, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ALMOST_RING [section, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ALMOST_RING.ARth [variable, in Coq.setoid_ring.InitialRing]
ZMORPHISM.ARth [variable, in Coq.setoid_ring.InitialRing]
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]
_ - _ [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]
ZMulOrderPropFunct [module, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.eq_mul_1 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.le_0_mul [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.le_mul_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.le_mul_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.le_0_square [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.le_mul_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_n1_neg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_diag_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_n1_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_1_mul_l [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_diag_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_n1_pos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_mul_r [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.lt_1_mul_neg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_nonpos [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_nonpos_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_nonneg_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_pos [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_nonpos_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_le_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_neg [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_nonneg [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.mul_lt_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.nlt_square_0 [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.square_nonneg [abbreviation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.square_le_simpl_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.square_lt_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.square_lt_simpl_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulOrderPropFunct.square_le_mono_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZMulOrder]
- 1 [notation, in Coq.Numbers.Integer.Abstract.ZMulOrder]
ZMulPropFunct [module, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_opp_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_sub_distr_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_opp_opp [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_sub_distr_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
ZMulPropFunct.mul_opp_l [lemma, in Coq.Numbers.Integer.Abstract.ZMul]
Zmult [definition, in Coq.ZArith.BinInt]
Zmult_le_compat [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat2 [lemma, in Coq.ZArith.Zorder]
Zmult_mod_distr_l [lemma, in Coq.ZArith.Zdiv]
Zmult_reg_l [lemma, in Coq.ZArith.BinInt]
Zmult_0_l [lemma, in Coq.ZArith.BinInt]
Zmult_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_minus_distr_r [lemma, in Coq.ZArith.BinInt]
Zmult_ge_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_mod [lemma, in Coq.ZArith.Zdiv]
Zmult_integral [lemma, in Coq.ZArith.BinInt]
Zmult_mod_distr_r [lemma, in Coq.ZArith.Zdiv]
Zmult_le_0_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_power [lemma, in Coq.ZArith.Zpow_facts]
Zmult_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_lt_compat [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_lt_b [lemma, in Coq.Numbers.BigNumPrelude]
Zmult_opp_opp [lemma, in Coq.ZArith.BinInt]
Zmult_1_l [lemma, in Coq.ZArith.BinInt]
Zmult_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_compare_compat_l [lemma, in Coq.ZArith.Zcompare]
Zmult_le_approx [lemma, in Coq.ZArith.auxiliary]
Zmult_minus_distr_l [lemma, in Coq.ZArith.BinInt]
Zmult_lt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_plus_distr_r [lemma, in Coq.ZArith.BinInt]
Zmult_comm [lemma, in Coq.ZArith.BinInt]
Zmult_integral_l [lemma, in Coq.ZArith.BinInt]
Zmult_lt_0_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_succ_r [lemma, in Coq.ZArith.BinInt]
Zmult_0_r [lemma, in Coq.ZArith.BinInt]
Zmult_divide_compat_r [lemma, in Coq.ZArith.Znumtheory]
Zmult_ge_compat [lemma, in Coq.ZArith.Zorder]
Zmult_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_1_inversion_l [lemma, in Coq.ZArith.BinInt]
Zmult_compare_compat_r [lemma, in Coq.ZArith.Zcompare]
Zmult_one [lemma, in Coq.ZArith.Znumtheory]
Zmult_succ_r_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_gt_0_reg_l [lemma, in Coq.ZArith.Zorder]
Zmult_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_divide_compat_l [lemma, in Coq.ZArith.Znumtheory]
Zmult_gt_0_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_lt_0_reg_r_2 [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleDiv]
Zmult_lt_O_compat [abbreviation, in Coq.ZArith.Zorder]
Zmult_gt_0_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zmult_gt_0_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_assoc [lemma, in Coq.ZArith.BinInt]
Zmult_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zmult_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_reg_r [lemma, in Coq.ZArith.BinInt]
Zmult_gt_0_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zmult_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_ge_compat_l [lemma, in Coq.ZArith.Zorder]
Zmult_opp_comm [lemma, in Coq.ZArith.BinInt]
Zmult_succ_l_reverse [lemma, in Coq.ZArith.BinInt]
Zmult_1_r [lemma, in Coq.ZArith.BinInt]
Zmult_succ_l [lemma, in Coq.ZArith.BinInt]
Zmult_permute [lemma, in Coq.ZArith.BinInt]
Zmult_ge_reg_r [lemma, in Coq.ZArith.Zorder]
Zmult_plus_distr_l [lemma, in Coq.ZArith.BinInt]
Zmult_gt_0_lt_0_reg_r [lemma, in Coq.ZArith.Zorder]
Znat [library]
ZNatPairs [library]
Zne [definition, in Coq.ZArith.BinInt]
Zneg [constructor, in Coq.ZArith.BinInt]
Zneg_xO [lemma, in Coq.ZArith.BinInt]
Zneg_plus_distr [lemma, in Coq.ZArith.BinInt]
Zneg_xI [lemma, in Coq.ZArith.BinInt]
Zneg' [definition, in Coq.omega.PreOmega]
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_lt_ge [lemma, in Coq.ZArith.Zorder]
Znot_ge_lt [lemma, in Coq.ZArith.Zorder]
Znot_gt_le [lemma, in Coq.ZArith.Zorder]
ZNpower [lemma, in Coq.micromega.ZMicromega]
Znumtheory [library]
znz [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_of_Z [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_is_even [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_pos_mod [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_gcd_gt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_1 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_pos.w [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_mod [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_opp [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_square_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_pred_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_div21 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_opp_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_div_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_0W [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sqrt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_succ [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_pred_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_op [record, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_add_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_div [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_of_pos.op_spec [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_pos.w_op [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_spec [record, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_opp_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_mul_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_compare [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_gcd [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_to_Z [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_sqrt2 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_square_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_head0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_of_pos_correct [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_digits [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_Bm1 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_opp_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add_carry_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_mul [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_pos_mod [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_gcd_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_gcd [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_pred [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_opp_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_div_gt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_sub [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add_mul_div [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_tail0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_mul_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_carry_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_add_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_W0 [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sqrt2 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sqrt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_pos [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_succ [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_zdigits [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_succ_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_opp [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_succ_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_digits [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_mul [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_pos [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_add_carry [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_is_even [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_zdigits [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_head0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_sub_carry_c [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_WW [definition, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_div21 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_add_mul_div [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_to_Z [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_1 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_compare [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_eq0 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_tail0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_Z_correct [lemma, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_mod_gt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_pred [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_of_pos [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_mod_gt [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_mod [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
znz_Bm1 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
znz_eq0 [projection, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
zn2z [inductive, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleType]
Zn2Z [section, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleType]
zn2z_to_Z [definition, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleType]
zn2z_word_comm [definition, in Coq.Numbers.Natural.BigN.Nbasic]
Zn2Z.znz [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleType]
Zodd [definition, in Coq.ZArith.Zeven]
Zodd_dec [definition, in Coq.ZArith.Zeven]
Zodd_plus_Zeven [lemma, in Coq.ZArith.Zeven]
Zodd_ex [lemma, in Coq.ZArith.Zeven]
Zodd_div2 [lemma, in Coq.ZArith.Zeven]
Zodd_not_Zeven [lemma, in Coq.ZArith.Zeven]
Zodd_bit_value [lemma, in Coq.ZArith.Zdigits]
Zodd_mult_Zodd [lemma, in Coq.ZArith.Zeven]
Zodd_div2_neg [lemma, in Coq.ZArith.Zeven]
Zodd_2p_plus_1 [lemma, in Coq.ZArith.Zeven]
Zodd_bool [definition, in Coq.ZArith.Zeven]
Zodd_plus_Zodd [lemma, in Coq.ZArith.Zeven]
Zodd_pred [lemma, in Coq.ZArith.Zeven]
Zodd_Sn [lemma, in Coq.ZArith.Zeven]
ZOdiv [definition, in Coq.ZArith.ZOdiv_def]
ZOdiv [library]
ZOdiv_lt_upper_bound [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_ZOdiv [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_unique [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_unique_full [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_opp_l [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_mult_cancel_r [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_sgn [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_1_r [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_eucl_correct [lemma, in Coq.ZArith.ZOdiv_def]
ZOdiv_0_r [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_opp_opp [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_mult_cancel_l [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_mult_le [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_le_upper_bound [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_eucl_Zdiv_eucl_pos [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_small [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_Zdiv_pos [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_le_lower_bound [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_0_l [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_eucl [definition, in Coq.ZArith.ZOdiv_def]
ZOdiv_mod_unique_full [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_opp_r [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_1_l [lemma, in Coq.ZArith.ZOdiv]
ZOdiv_def [library]
ZOmega [module, in Coq.romega.ReflOmegaCore]
ZOmod [definition, in Coq.ZArith.ZOdiv_def]
ZOmod_lt_neg_pos [lemma, in Coq.ZArith.ZOdiv]
ZOmod_0_r [lemma, in Coq.ZArith.ZOdiv]
ZOmod_le [lemma, in Coq.ZArith.ZOdiv]
ZOmod_Zmod_zero [lemma, in Coq.ZArith.ZOdiv]
ZOmod_unique [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt_pos_pos [lemma, in Coq.ZArith.ZOdiv]
ZOmod_1_l [lemma, in Coq.ZArith.ZOdiv]
ZOmod_0_l [lemma, in Coq.ZArith.ZOdiv]
ZOmod_opp_opp [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt_pos_neg [lemma, in Coq.ZArith.ZOdiv]
ZOmod_small [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt_neg [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt_pos [lemma, in Coq.ZArith.ZOdiv]
ZOmod_sgn [lemma, in Coq.ZArith.ZOdiv]
ZOmod_opp_l [lemma, in Coq.ZArith.ZOdiv]
ZOmod_Zmod_pos [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt_neg_neg [lemma, in Coq.ZArith.ZOdiv]
ZOmod_lt [lemma, in Coq.ZArith.ZOdiv]
ZOmod_opp_r [lemma, in Coq.ZArith.ZOdiv]
ZOmod_mod [lemma, in Coq.ZArith.ZOdiv]
ZOmod_divides [lemma, in Coq.ZArith.ZOdiv]
ZOmod_1_r [lemma, in Coq.ZArith.ZOdiv]
ZOmod_sgn2 [lemma, in Coq.ZArith.ZOdiv]
ZOmod_unique_full [lemma, in Coq.ZArith.ZOdiv]
ZOmult_mod_distr_l [lemma, in Coq.ZArith.ZOdiv]
ZOmult_mod [lemma, in Coq.ZArith.ZOdiv]
ZOmult_mod_idemp_l [lemma, in Coq.ZArith.ZOdiv]
ZOmult_mod_idemp_r [lemma, in Coq.ZArith.ZOdiv]
ZOmult_mod_distr_r [lemma, in Coq.ZArith.ZOdiv]
Zone_min_pos [lemma, in Coq.ZArith.Zbool]
Zone_pos [lemma, in Coq.ZArith.Zbool]
Zone_divide [lemma, in Coq.ZArith.Znumtheory]
ZOplus_mod [lemma, in Coq.ZArith.ZOdiv]
ZOplus_mod_idemp_l [lemma, in Coq.ZArith.ZOdiv]
ZOplus_mod_idemp_r [lemma, in Coq.ZArith.ZOdiv]
Zopp [definition, in Coq.ZArith.BinInt]
Zopp_succ [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_l [lemma, in Coq.ZArith.BinInt]
Zopp_eq_mult_neg_1 [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_r [lemma, in Coq.ZArith.BinInt]
Zopp_involutive [lemma, in Coq.ZArith.BinInt]
Zopp_inj [lemma, in Coq.ZArith.BinInt]
Zopp_mult_distr_l_reverse [lemma, in Coq.ZArith.BinInt]
Zopp_plus_distr [lemma, in Coq.ZArith.BinInt]
Zopp_neg [lemma, in Coq.ZArith.BinInt]
Zopp_0 [lemma, in Coq.ZArith.BinInt]
ZOrder [module, in Coq.ZArith.ZOrderedType]
Zorder [library]
ZOrderedType [library]
ZOrderPropFunct [module, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.le_pred_lt_succ [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.le_pred_lt [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.le_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.le_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.le_succ_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_pred_lt [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_pred_le [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_le_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_n1_r [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_lt_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_succ_lt_pred [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.lt_pred_lt_succ [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.neg_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.neg_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.neq_pred_l [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.nle_pred_r [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.nonpos_pos_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.nonpos_nonneg_cases [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.pred_le_mono [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZOrderPropFunct.pred_lt_mono [lemma, in Coq.Numbers.Integer.Abstract.ZLt]
ZO_div_plus_l [lemma, in Coq.ZArith.ZOdiv]
ZO_div_mod_eq [lemma, in Coq.ZArith.ZOdiv]
ZO_div_pos [lemma, in Coq.ZArith.ZOdiv]
ZO_mod_same [lemma, in Coq.ZArith.ZOdiv]
ZO_div_same [lemma, in Coq.ZArith.ZOdiv]
ZO_div_monotone [lemma, in Coq.ZArith.ZOdiv]
ZO_mod_mult [lemma, in Coq.ZArith.ZOdiv]
ZO_div_plus [lemma, in Coq.ZArith.ZOdiv]
ZO_div_monotone_pos [lemma, in Coq.ZArith.ZOdiv]
ZO_div_exact_full_2 [lemma, in Coq.ZArith.ZOdiv]
ZO_mult_div_le [lemma, in Coq.ZArith.ZOdiv]
ZO_div_mult [lemma, in Coq.ZArith.ZOdiv]
ZO_mod_plus [lemma, in Coq.ZArith.ZOdiv]
ZO_div_lt [lemma, in Coq.ZArith.ZOdiv]
ZO_mult_div_ge [lemma, in Coq.ZArith.ZOdiv]
ZO_div_exact_full_1 [lemma, in Coq.ZArith.ZOdiv]
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_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.add_0_l [lemma, 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_nge [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_succ_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_eq_cases [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_irrefl [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.lt_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.max_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.min_r [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_0_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_comm [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.mul_succ_l [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.NPropMod [module, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp [definition, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp_0 [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.opp_succ [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_wd [instance, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.pred_succ [lemma, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
ZPairsAxiomsMod.sub [definition, 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_succ_r [lemma, 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.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.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.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]
_ <= _ (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]
Zplus [definition, in Coq.ZArith.BinInt]
Zplus_le_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_succ_r [abbreviation, in Coq.ZArith.BinInt]
Zplus_compare_compat [lemma, in Coq.ZArith.Zcompare]
Zplus_succ_r_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_min_distr_r [definition, in Coq.ZArith.Zmin]
Zplus_comm [lemma, in Coq.ZArith.BinInt]
Zplus_le_lt_compat [lemma, in Coq.ZArith.Zorder]
Zplus_max_distr_l [definition, in Coq.ZArith.Zmax]
Zplus_le_0_compat [lemma, in Coq.ZArith.Zorder]
Zplus_0_simpl_l [lemma, in Coq.ZArith.BinInt]
Zplus_mod_idemp_l [lemma, in Coq.ZArith.Zdiv]
Zplus_le_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_gt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_gt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_minus [lemma, in Coq.ZArith.BinInt]
Zplus_lt_compat_l [lemma, in Coq.ZArith.Zorder]
Zplus_assoc [lemma, in Coq.ZArith.BinInt]
Zplus_mod [lemma, in Coq.ZArith.Zdiv]
Zplus_lt_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_reg_l [lemma, in Coq.ZArith.BinInt]
Zplus_0_simpl_l_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_0_r [lemma, in Coq.ZArith.BinInt]
Zplus_succ_comm [lemma, in Coq.ZArith.BinInt]
Zplus_mod_idemp_r [lemma, in Coq.ZArith.Zdiv]
Zplus_0_l [lemma, in Coq.ZArith.BinInt]
Zplus_minus_eq [lemma, in Coq.ZArith.BinInt]
Zplus_max_distr_r [definition, in Coq.ZArith.Zmax]
Zplus_lt_le_compat [lemma, in Coq.ZArith.Zorder]
Zplus_eq_compat [lemma, in Coq.ZArith.BinInt]
Zplus_gt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_opp_l [lemma, in Coq.ZArith.BinInt]
Zplus_permute [lemma, in Coq.ZArith.BinInt]
Zplus_gt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_opp_expand [lemma, in Coq.ZArith.BinInt]
Zplus_mod_one [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt]
Zplus_le_compat [lemma, in Coq.ZArith.Zorder]
Zplus_lt_reg_r [lemma, in Coq.ZArith.Zorder]
Zplus_diag_eq_mult_2 [lemma, in Coq.ZArith.BinInt]
Zplus_succ_l [lemma, in Coq.ZArith.BinInt]
Zplus_opp_r [lemma, in Coq.ZArith.BinInt]
Zplus_assoc_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_lt_compat_r [lemma, in Coq.ZArith.Zorder]
Zplus_le_reg_l [lemma, in Coq.ZArith.Zorder]
Zplus_0_r_reverse [lemma, in Coq.ZArith.BinInt]
Zplus_lt_compat [lemma, in Coq.ZArith.Zorder]
Zplus' [definition, in Coq.ZArith.BinInt]
ZPminus [definition, in Coq.ZArith.BinInt]
ZPminus_spec [lemma, in Coq.micromega.EnvRing]
ZPminus_spec [lemma, in Coq.setoid_ring.Ring_polynom]
Zpos [constructor, in Coq.ZArith.BinInt]
Zpos_minus_morphism [lemma, in Coq.ZArith.BinInt]
Zpos_xI [lemma, in Coq.ZArith.BinInt]
Zpos_eq [lemma, in Coq.ZArith.BinInt]
Zpos_min [definition, in Coq.ZArith.Zmin]
Zpos_eq_Z_of_nat_o_nat_of_P [lemma, in Coq.ZArith.Znat]
Zpos_eq_rev [lemma, in Coq.ZArith.BinInt]
Zpos_plus_distr [lemma, in Coq.ZArith.BinInt]
Zpos_max_1 [definition, in Coq.ZArith.Zmax]
Zpos_eq_iff [lemma, in Coq.ZArith.BinInt]
Zpos_xO [lemma, in Coq.ZArith.BinInt]
Zpos_succ_morphism [lemma, in Coq.ZArith.BinInt]
Zpos_P_of_succ_nat [lemma, in Coq.ZArith.Znat]
Zpos_minus [definition, in Coq.ZArith.Zmax]
Zpos_mult_morphism [lemma, in Coq.ZArith.BinInt]
Zpos_max [definition, in Coq.ZArith.Zmax]
Zpos_minus [lemma, in Coq.ZArith.Zminmax]
Zpos' [definition, in Coq.omega.PreOmega]
Zpower [definition, in Coq.ZArith.Zpow_def]
Zpower [library]
Zpower_gt_0 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_1_r [lemma, in Coq.ZArith.Zpow_facts]
Zpower_1_r [lemma, in Coq.ZArith.Zpow_facts]
Zpower_nat_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_ge_0 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone2 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_0_l [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_nat [lemma, in Coq.ZArith.Zpower]
Zpower_pos [definition, in Coq.ZArith.Zpow_def]
Zpower_nat [definition, in Coq.ZArith.Zpower]
Zpower_mult [lemma, in Coq.ZArith.Zpow_facts]
Zpower_NR0 [lemma, in Coq.Reals.Rfunctions]
Zpower_pos_0_l [lemma, in Coq.ZArith.Zpow_facts]
Zpower_pos_1_l [lemma, in Coq.ZArith.Zpow_facts]
Zpower_le_monotone [lemma, in Coq.ZArith.Zpow_facts]
Zpower_exp [lemma, in Coq.ZArith.Zpower]
Zpower_Zsucc [lemma, in Coq.ZArith.Zpow_facts]
Zpower_Zabs [lemma, in Coq.ZArith.Zpow_facts]
Zpower_0_r [lemma, in Coq.ZArith.Zpow_facts]
Zpower_Qpower [lemma, in Coq.QArith.Qpower]
Zpower_pos_powerRZ [lemma, in Coq.Reals.Rfunctions]
Zpower_pos_pos [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_divide [lemma, in Coq.ZArith.Zpow_facts]
Zpower_theory [lemma, in Coq.ZArith.Zpow_def]
Zpower_le_monotone_inv [lemma, in Coq.ZArith.Zpow_facts]
Zpower_mod [lemma, in Coq.ZArith.Zpow_facts]
Zpower_nat_Zpower [lemma, in Coq.ZArith.Zpow_facts]
Zpower_2 [lemma, in Coq.ZArith.Zpow_facts]
Zpower_nat_powerRZ_absolu [lemma, in Coq.Reals.Rfunctions]
Zpower_pos_is_exp [lemma, in Coq.ZArith.Zpower]
Zpower_nat_powerRZ [lemma, in Coq.Reals.Rfunctions]
Zpower_1_l [lemma, in Coq.ZArith.Zpow_facts]
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]
Zpow_mod [definition, in Coq.ZArith.Zpow_facts]
Zpow_mod_pos [definition, in Coq.ZArith.Zpow_facts]
Zpow_mod_correct [lemma, in Coq.ZArith.Zpow_facts]
Zpow_mod_pos_correct [lemma, in Coq.ZArith.Zpow_facts]
Zpow_facts [library]
Zpow_def [library]
Zpred [definition, in Coq.ZArith.BinInt]
Zpred_pred' [lemma, in Coq.ZArith.BinInt]
Zpred_succ [lemma, in Coq.ZArith.BinInt]
Zpred' [definition, in Coq.ZArith.BinInt]
Zpred'_inj [lemma, in Coq.ZArith.BinInt]
Zpred'_succ' [lemma, in Coq.ZArith.BinInt]
ZProperties [library]
ZPropFunct [module, in Coq.Numbers.Integer.Abstract.ZProperties]
ZPropSig [module, in Coq.Numbers.Integer.Abstract.ZProperties]
Zred_factor0 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor5 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor3 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor1 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor6 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor4 [lemma, in Coq.omega.OmegaLemmas]
Zred_factor2 [lemma, in Coq.omega.OmegaLemmas]
Zrel_prime_neq_mod_0 [lemma, in Coq.ZArith.Znumtheory]
Zri [instance, in Coq.nsatz.Nsatz]
Zring_morph [lemma, in Coq.micromega.ZCoeff]
Zsgn [definition, in Coq.ZArith.BinInt]
ZSgnAbs [library]
ZSgnAbsPropSig [module, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_involutive [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_0 [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_pos [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_eq_or_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_eq_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_sgn [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_case [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_triangle [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_mul [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_0_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_square [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_neq_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_case_strong [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_eq_cases [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_wd [instance, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_max [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_neq' [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_or_opp_abs [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_spec [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_sub_triangle [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.abs_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_null_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_spec [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_abs [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_0 [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_opp [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_neg_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_nonneg [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_nonpos [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_mul [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_wd [instance, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
ZSgnAbsPropSig.sgn_pos_iff [lemma, in Coq.Numbers.Integer.Abstract.ZSgnAbs]
Zsgn_Zmult [lemma, in Coq.ZArith.Zabs]
Zsgn_spec [lemma, in Coq.ZArith.Zabs]
Zsgn_pos [lemma, in Coq.ZArith.Zabs]
Zsgn_pos_iff [lemma, in Coq.ZArith.ZOdiv]
Zsgn_Zopp [lemma, in Coq.ZArith.Zabs]
Zsgn_neg [lemma, in Coq.ZArith.Zabs]
Zsgn_Zabs [lemma, in Coq.ZArith.Zabs]
Zsgn_null [lemma, in Coq.ZArith.Zabs]
ZSig [library]
ZSigZAxioms [library]
Zsor [lemma, in Coq.micromega.ZMicromega]
ZSORaddon [lemma, in Coq.micromega.ZMicromega]
Zsplit2 [lemma, in Coq.ZArith.Zeven]
Zsqrt [definition, in Coq.ZArith.Zsqrt]
Zsqrt [library]
Zsqrt_interval [lemma, in Coq.ZArith.Zsqrt]
Zsqrt_plain [definition, in Coq.ZArith.Zsqrt]
Zsqrt_le [lemma, in Coq.ZArith.Zsqrt]
Zsqrt_square_id [lemma, in Coq.ZArith.Zsqrt]
Zsqrt_plain_is_pos [lemma, in Coq.ZArith.Zsqrt]
Zsquare [definition, in Coq.ZArith.Zpow_facts]
Zsquare_mult [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt]
Zsquare_correct [lemma, in Coq.ZArith.Zpow_facts]
Zsquare_pos [lemma, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleSqrt]
Zsquare_le [lemma, in Coq.Numbers.BigNumPrelude]
Zsth [lemma, in Coq.setoid_ring.InitialRing]
Zsucc [definition, in Coq.ZArith.BinInt]
Zsucc_pred [lemma, in Coq.ZArith.BinInt]
Zsucc_gt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_lt_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_succ' [lemma, in Coq.ZArith.BinInt]
Zsucc_inj_contrapositive [lemma, in Coq.ZArith.BinInt]
Zsucc_gt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_le_reg [lemma, in Coq.ZArith.Zorder]
Zsucc_le_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_max_distr [definition, in Coq.ZArith.Zmax]
Zsucc_lt_compat [lemma, in Coq.ZArith.Zorder]
Zsucc_min_distr [definition, in Coq.ZArith.Zmin]
Zsucc_discr [lemma, in Coq.ZArith.BinInt]
Zsucc_inj [lemma, in Coq.ZArith.BinInt]
Zsucc_eq_compat [lemma, in Coq.ZArith.BinInt]
Zsucc' [definition, in Coq.ZArith.BinInt]
Zsucc'_pred' [lemma, in Coq.ZArith.BinInt]
Zsucc'_discr [lemma, in Coq.ZArith.BinInt]
Zsucc'_inj [lemma, in Coq.ZArith.BinInt]
ZTautoChecker [definition, in Coq.micromega.ZMicromega]
ZTautoChecker_sound [lemma, in Coq.micromega.ZMicromega]
Zth [lemma, in Coq.setoid_ring.InitialRing]
ZTheory [definition, in Coq.ring.LegacyZArithRing]
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]
ZType [module, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZTypeIsZAxioms [module, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.abs_eq [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.abs_neq [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.add_succ_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.add_0_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.add_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.bi_induction [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.BP [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.BS [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.B_holds [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.B0 [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.compare_spec [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.compare_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.div_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.div_mod [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.eqb [definition, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.eqb_eq [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.eq_equiv [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction [section, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction.A [variable, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction.AS [variable, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction.A_wd [variable, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction.A0 [variable, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.Induction.B [variable, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.lt_eq_cases [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.lt_irrefl [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.lt_succ_r [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.lt_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.max_r [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.max_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.min_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.min_r [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mod_pos_bound [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mod_neg_bound [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mod_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mul_succ_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mul_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.mul_0_l [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.opp_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.opp_0 [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.opp_succ [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.pred_succ [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.pred_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sgn_null [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sgn_pos [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sgn_neg [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sub_0_r [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sub_succ_r [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.sub_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.succ_pred [lemma, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
ZTypeIsZAxioms.succ_wd [instance, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
_ < _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
- _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
_ <= _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
_ * _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
_ - _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
_ + _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
0 [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
[ _ ] [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType_Notation [module, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType_ZAxioms [module, in Coq.Numbers.Integer.SpecViaZ.ZSigZAxioms]
_ == _ [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType' [module, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.abs [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.add [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.compare [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.div [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.div_eucl [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.eq [definition, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.eq_bool [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.gcd [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.le [definition, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.lt [definition, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.max [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.min [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.minus_one [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.modulo [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.mul [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.of_Z [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.one [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.opp [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.power [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.power_pos [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.pred [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.sgn [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_1 [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_max [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_sub [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_succ [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_div [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_square [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_compare [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_m1 [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_min [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_add [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_eq_bool [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_gcd [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_sgn [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_opp [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_div_eucl [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_mul [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_modulo [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_of_Z [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_0 [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_power_pos [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_sqrt [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_abs [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_pred [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.spec_power [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.sqrt [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.square [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.sub [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.succ [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.t [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.to_Z [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
ZType.zero [axiom, in Coq.Numbers.Integer.SpecViaZ.ZSig]
[ _ ] [notation, in Coq.Numbers.Integer.SpecViaZ.ZSig]
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_well_founded [lemma, in Coq.ZArith.Zwf]
Zwf_up [definition, in Coq.ZArith.Zwf]
ZWitness [definition, in Coq.micromega.ZMicromega]
Z_to_two_compl [lemma, in Coq.ZArith.Zdigits]
Z_2nZ.spec_ww_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_le [lemma, in Coq.ZArith.Zdiv]
Z_BRIC_A_BRAC [section, in Coq.ZArith.Zdigits]
Z_nZ_Spec.w_gcd_gt [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ._zn2z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_pred_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_modulo_2 [lemma, in Coq.ZArith.Zeven]
Z_nZ_Spec.w_add_mul_div [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_div_mod_eq_full [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.wwB [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.i2z_opp [lemma, in Coq.ZArith.Int]
Z_2nZ.w_add_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.opp_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_UBE.eqb_eq [definition, in Coq.ZArith.ZOrderedType]
Z_2nZ.w_to_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.mod_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.eq0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_UBE [module, in Coq.ZArith.ZOrderedType]
Z_nZ_Spec.w_add [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_OT.lt_compat [instance, in Coq.ZArith.ZOrderedType]
Z_of_N_succ [lemma, in Coq.NArith.Nnat]
Z_of_N_eq_rev [lemma, in Coq.NArith.Nnat]
Z_2nZ.spec_ww_sub_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_pos_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_pred_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.sub [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_UBE.t [definition, in Coq.ZArith.ZOrderedType]
Z_as_Int.mult_lt_compat_l [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.w_0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_karatsuba_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.sqrt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_to_binary [lemma, in Coq.ZArith.Zdigits]
Z_nZ_Spec.w_pred [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.i2z_minus [lemma, in Coq.ZArith.Int]
Z_2nZ.spec_ww_gcd [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int._3 [definition, in Coq.ZArith.Int]
Z_mod_nz_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_mod_gt [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.w_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.ww_Bm1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int._1 [definition, in Coq.ZArith.Int]
Z_of_nat_set [lemma, in Coq.ZArith.Wf_Z]
Z_2nZ.spec_ww_is_even [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT [module, in Coq.ZArith.ZOrderedType]
Z_as_Int.i2z_plus [lemma, in Coq.ZArith.Int]
Z_2nZ.spec_ww_of_pos [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_tail0 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.square_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.one [definition, in Coq.romega.ReflOmegaCore]
Z_nZ_Spec.w_sub_carry [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[+| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_OT.le_lteq [definition, in Coq.ZArith.ZOrderedType]
Z_as_OT [module, in Coq.Structures.OrderedTypeEx]
Z_of_N_of_nat [lemma, in Coq.NArith.Nnat]
Z_2nZ.spec_ww_div21 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.compare [definition, in Coq.ZArith.ZOrderedType]
Z_2nZ.spec_ww_succ [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_opp_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w1 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_div_plus [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.lt_not_eq [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.mod_ [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.add_mul_div [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_notzerop [lemma, in Coq.ZArith.ZArith_dec]
Z_2nZ.w_succ_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_digits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_w_div32 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int [module, in Coq.romega.ReflOmegaCore]
Z_2nZ.spec_ww_head0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_pos_mod [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_mult_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_gt_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_as_Int.plus [definition, in Coq.romega.ReflOmegaCore]
Z_of_N_ge_rev [lemma, in Coq.NArith.Nnat]
Z_as_OT.lt [definition, in Coq.ZArith.ZOrderedType]
Z_2nZ.compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_ge [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_div_gt [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_nZ_Spec.w_opp_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_low [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_gt_rev [lemma, in Coq.NArith.Nnat]
Z_2nZ.head0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.le [definition, in Coq.ZArith.ZOrderedType]
Z_2nZ.add_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_opp_carry [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.opp [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.w_head0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_of_pos [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
[+| _ |] [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.ge [definition, in Coq.romega.ReflOmegaCore]
z_of_bigint [definition, in Coq.extraction.ExtrOcamlBigIntConv]
Z_mod_plus_full [lemma, in Coq.ZArith.Zdiv]
Z_of_N' [definition, in Coq.omega.PreOmega]
Z_of_nat [definition, in Coq.ZArith.BinInt]
Z_2nZ.spec_ww_pred [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.ge_lt_dec [definition, in Coq.ZArith.Int]
Z_as_Int.compare_Eq [definition, in Coq.romega.ReflOmegaCore]
Z_lt_abs_induction [lemma, in Coq.ZArith.Zcomplements]
Z_2nZ.sub_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_tail0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.div32 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_op [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_mult [lemma, in Coq.ZArith.Zdiv]
Z_le_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_2nZ.spec_ww_div_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_div [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_digits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.int [definition, in Coq.ZArith.Int]
Z_nZ_Spec.w_compare [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int [module, in Coq.ZArith.Int]
Z_nZ_Spec [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_mod_mult [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.sub_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_exact_2 [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.lt_trans [definition, in Coq.romega.ReflOmegaCore]
Z_of_N_le [lemma, in Coq.NArith.Nnat]
[|| _ ||] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.i2z_1 [lemma, in Coq.ZArith.Int]
Z_nZ_Spec.w_zdigits [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_div_zero_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.compare_Lt [lemma, in Coq.romega.ReflOmegaCore]
Z_as_Int.opp_le_compat [lemma, in Coq.romega.ReflOmegaCore]
Z_of_N_pos [lemma, in Coq.NArith.Nnat]
Z_of_N_plus [lemma, in Coq.NArith.Nnat]
Z_as_OT.lt_trans [lemma, in Coq.Structures.OrderedTypeEx]
Z_div_same [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_sub_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_ww_tail00 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_to_binary_Sn [lemma, in Coq.ZArith.Zdigits]
Z_div_exact_full_2 [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.spec_ww_Bm1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.minus [definition, in Coq.ZArith.Int]
Z_2nZ.w_add_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.wB [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_to_two_compl_Sn_z [lemma, in Coq.ZArith.Zdigits]
Z_2nZ.spec_ww_sub_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.opp [definition, in Coq.ZArith.Int]
Z_lt_rec [lemma, in Coq.ZArith.Wf_Z]
Z_2nZ.w_sub_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_gt_iff [lemma, in Coq.NArith.Nnat]
Z_of_N_gt [lemma, in Coq.NArith.Nnat]
Z_nZ_Spec.w_add_carry_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_to_two_compl_to_Z [lemma, in Coq.ZArith.Zdigits]
Z_2nZ.spec_ww_add_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_Bm2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
[[ _ ]] [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.mul_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.op_spec [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_mul_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_OT [module, in Coq.Structures.OrdersEx]
Z_2nZ.ww_of_pos [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_nat_prop [lemma, in Coq.ZArith.Wf_Z]
Z_2nZ.spec_ww_square_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_succ [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.karatsuba_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_pos [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.w_of_pos [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_plus_full [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.w_pred [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_mod_neg [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_square_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_OT.t [definition, in Coq.Structures.OrderedTypeEx]
Z_2nZ.ww_1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.gt [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.spec_ww_succ_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_div21 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.tail0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_eq_mult [lemma, in Coq.ZArith.BinInt]
Z_of_N [definition, in Coq.ZArith.BinInt]
Z_2nZ.w_is_even [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_sqrt [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_ww_compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_eq_iff [lemma, in Coq.NArith.Nnat]
Z_2nZ.w_eq0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_opp_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_lt [lemma, in Coq.ZArith.Zdiv]
Z_div_mod [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.gcd_gt_fix [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_mod_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_div_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.eq [definition, in Coq.Structures.OrderedTypeEx]
Z_div_plus_l [definition, in Coq.Numbers.BigNumPrelude]
Z_div_mod_full [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.spec_ww_sqrt2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_minus [lemma, in Coq.NArith.Nnat]
Z_nZ_Spec.w_succ_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.i2z_3 [lemma, in Coq.ZArith.Int]
[| _ |] [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_square_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_min [lemma, in Coq.NArith.Nnat]
Z_as_UBE.eqb [definition, in Coq.ZArith.ZOrderedType]
Z_as_Int.mult [definition, in Coq.romega.ReflOmegaCore]
Z_nZ_Spec.w_mod [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_mod_nz_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.spec_ww_eq0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_gcd [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_dec' [lemma, in Coq.ZArith.ZArith_dec]
Z_lt_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_2nZ.to_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w0 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_div2_value [lemma, in Coq.ZArith.Zdigits]
Z_lt_induction [lemma, in Coq.ZArith.Wf_Z]
Z_R_minus [lemma, in Coq.Reals.RIneq]
Z_as_Int.le_lt_iff [lemma, in Coq.romega.ReflOmegaCore]
Z_2nZ.pred [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.sqrt2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_to_binary_to_Z [lemma, in Coq.ZArith.Zdigits]
Z_le_lt_eq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_nZ_Spec.w [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.pos_mod [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_succ [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.w_gcd [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.opp [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_is_even [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.ge_le_iff [definition, in Coq.romega.ReflOmegaCore]
Z_as_Int.plus [definition, in Coq.ZArith.Int]
Z_2nZ.div21 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.ww_WW [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_nz_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.spec_ww_div [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.sub_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_le_iff [lemma, in Coq.NArith.Nnat]
Z_div_nz_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_mod_zero_opp_full [lemma, in Coq.ZArith.Zdiv]
Z_as_DT [module, in Coq.ZArith.ZOrderedType]
Z_2nZ.add [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_lt_ge_bool [definition, in Coq.ZArith.Zbool]
Z_nZ_Spec.w_div [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.plus_le_compat [definition, in Coq.romega.ReflOmegaCore]
Z_of_nat_of_N [lemma, in Coq.NArith.Nnat]
Z_nZ_Spec.w_opp [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.i2z_eq [lemma, in Coq.ZArith.Int]
Z_nZ_Spec.w_sub [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_mod_plus [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_head0 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.div_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_gt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_of_N_abs [lemma, in Coq.NArith.Nnat]
Z_mod_lt [lemma, in Coq.ZArith.Zdiv]
Z_of_N_max [lemma, in Coq.NArith.Nnat]
Z_as_Int.i2z_max [lemma, in Coq.ZArith.Int]
Z_2nZ.spec_ww_sub_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_eq_dec [definition, in Coq.ZArith.ZArith_dec]
Z_div_mod_eq [lemma, in Coq.ZArith.Zdiv]
Z_as_OT.eq_trans [definition, in Coq.Structures.OrderedTypeEx]
Z_ge_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_2nZ.succ_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_mod_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_zerop [lemma, in Coq.ZArith.ZArith_dec]
Z_as_Int._2 [definition, in Coq.ZArith.Int]
Z_as_Int._0 [definition, in Coq.ZArith.Int]
Z_2nZ.spec_add2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_same_full [lemma, in Coq.ZArith.Zdiv]
Z_noteq_dec [lemma, in Coq.ZArith.ZArith_dec]
z_of_int [definition, in Coq.extraction.ExtrOcamlIntConv]
Z_as_UBE.eq [definition, in Coq.ZArith.ZOrderedType]
Z_2nZ.spec_ww_mul_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_add_carry [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_nZ_Op [section, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ [section, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_le_gt_bool [definition, in Coq.ZArith.Zbool]
Z_to_binary_Sn_z [lemma, in Coq.ZArith.Zdigits]
Z_2nZ.w_sub [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_eq0 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_ww_to_Z [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_mod_zero_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.i2z_0 [lemma, in Coq.ZArith.Int]
Z_2nZ.add_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_div21 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.ring [lemma, in Coq.romega.ReflOmegaCore]
Z_as_Int.lt_0_1 [definition, in Coq.romega.ReflOmegaCore]
[| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.pred_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_to_Z [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.w_WW [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.gt_le_dec [definition, in Coq.ZArith.Int]
Z_2nZ.w_opp_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_plus_full_l [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.max [definition, in Coq.ZArith.Int]
Z_as_OT.lt_not_eq [lemma, in Coq.Structures.OrderedTypeEx]
Z_2nZ.gcd_cont [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.ww_0W [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_N_ge [lemma, in Coq.NArith.Nnat]
Z_2nZ.w_gcd_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_lt_dec [definition, in Coq.ZArith.ZArith_dec]
Z_div_exact_1 [lemma, in Coq.ZArith.Zdiv]
Z_div_mod_POS [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.le [definition, in Coq.romega.ReflOmegaCore]
[-| _ |] [notation, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.lt [definition, in Coq.Structures.OrderedTypeEx]
Z_2nZ.low [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_mul_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_add [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.le_lt_int [lemma, in Coq.romega.ReflOmegaCore]
Z_of_N_le_rev [lemma, in Coq.NArith.Nnat]
Z_to_two_compl_Sn [lemma, in Coq.ZArith.Zdigits]
Z_eq_bool [definition, in Coq.ZArith.Zbool]
Z_of_N_eq [lemma, in Coq.NArith.Nnat]
Z_2nZ.w_add [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
[-| _ |] [notation, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_nZ_Spec.wBm1 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_of_N_lt_rev [lemma, in Coq.NArith.Nnat]
Z_lt_le_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_nZ_Spec.w_op [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.compare [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.gcd_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_ge_dec [definition, in Coq.ZArith.ZArith_dec]
Z_2nZ.w_mul [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_noteq_bool [definition, in Coq.ZArith.Zbool]
Z_as_Int.eq_dec [definition, in Coq.ZArith.Int]
Z_2nZ.w [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.wB [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.gcd [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_0W [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_dec [lemma, in Coq.ZArith.ZArith_dec]
Z_as_Int.i2z_mult [lemma, in Coq.ZArith.Int]
Z_mult_div_ge_neg [lemma, in Coq.ZArith.Zdiv]
Z_of_nat_complete [lemma, in Coq.ZArith.Wf_Z]
Z_2nZ.w_Bm1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_ge0 [lemma, in Coq.ZArith.Zdiv]
Z_nZ_Spec.w_digits [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_ww_opp_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_head00 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.succ [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_sub_carry_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_of_N_le_0 [lemma, in Coq.NArith.Nnat]
Z_as_OT.compare [definition, in Coq.Structures.OrderedTypeEx]
Z_lt_abs_rec [lemma, in Coq.ZArith.Zcomplements]
Z_2nZ.div [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.compare_spec [definition, in Coq.ZArith.ZOrderedType]
Z_as_Int.i2z_2 [lemma, in Coq.ZArith.Int]
Z_of_nat_complete_inf [lemma, in Coq.ZArith.Wf_Z]
Z_2nZ.w_opp [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_mod_same_full [lemma, in Coq.ZArith.Zdiv]
Z_as_Int.gt_lt_iff [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.w_compare [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_mult_full [lemma, in Coq.ZArith.Zdiv]
Z_div_exact_full_1 [lemma, in Coq.ZArith.Zdiv]
Z_mod_zero_opp [lemma, in Coq.ZArith.Zdiv]
Z_as_OT.eq_refl [definition, in Coq.Structures.OrderedTypeEx]
Z_2nZ.spec_ww_opp [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_add_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_ge_lt_bool [definition, in Coq.ZArith.Zbool]
Z_as_Int.minus [definition, in Coq.romega.ReflOmegaCore]
Z_2nZ.w_sub_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.ww_W0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_div_zero_opp_r [lemma, in Coq.ZArith.Zdiv]
Z_2nZ._ww_digits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_mod_remainder [lemma, in Coq.ZArith.Zdiv]
Z_2nZ.spec_ww_tail0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_nZ_Spec.w_mul [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.is_even [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_1 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_add_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.mult [definition, in Coq.ZArith.Int]
Z_2nZ.spec_ww_mul [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_le_dec [definition, in Coq.ZArith.ZArith_dec]
Z_2nZ.w_add2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ._ww_zdigits [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_add_mul_div [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_of_nat' [definition, in Coq.omega.PreOmega]
Z_2nZ.spec_ww_add_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.mul [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.compare_Gt [lemma, in Coq.romega.ReflOmegaCore]
Z_nZ_Op.znz [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_OT.lt_strorder [instance, in Coq.ZArith.ZOrderedType]
Z_2nZ.w_sqrt2 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.eq_dec [definition, in Coq.Structures.OrderedTypeEx]
Z_2nZ.w_sub_carry_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.zero [definition, in Coq.romega.ReflOmegaCore]
Z_mod_same [lemma, in Coq.ZArith.Zdiv]
Z_as_DT [module, in Coq.Structures.OrdersEx]
Z_nZ_Spec.w_sqrt2 [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_as_Int.lt [definition, in Coq.romega.ReflOmegaCore]
Z_nZ_Spec.w_pred_c [variable, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
Z_2nZ.spec_ww_gcd_gt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.add_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_DT [module, in Coq.Structures.DecidableTypeEx]
Z_of_N_mult [lemma, in Coq.NArith.Nnat]
Z_of_N_lt_iff [lemma, in Coq.NArith.Nnat]
Z_of_N_lt [lemma, in Coq.NArith.Nnat]
Z_2nZ.spec_ww_sqrt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.w_sqrt [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_Int.int [definition, in Coq.romega.ReflOmegaCore]
Z_as_Int.i2z [definition, in Coq.ZArith.Int]
Z_gt_le_bool [definition, in Coq.ZArith.Zbool]
Z_2nZ.w_add_c [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.opp_carry [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_as_OT.eq_sym [definition, in Coq.Structures.OrderedTypeEx]
Z_of_N_ge_iff [lemma, in Coq.NArith.Nnat]
Z_2nZ.w_W0 [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z_2nZ.spec_ww_sub [variable, in Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic]
Z.minus_min_distr_l [lemma, in Coq.ZArith.Zminmax]
Z.minus_max_distr_r [lemma, in Coq.ZArith.Zminmax]
Z.minus_min_distr_r [lemma, in Coq.ZArith.Zminmax]
Z.minus_max_distr_l [lemma, in Coq.ZArith.Zminmax]
Z.opp_max_distr [lemma, in Coq.ZArith.Zminmax]
Z.opp_min_distr [lemma, in Coq.ZArith.Zminmax]
Z.plus_max_distr_l [lemma, in Coq.ZArith.Zminmax]
Z.plus_min_distr_l [lemma, in Coq.ZArith.Zminmax]
Z.plus_min_distr_r [lemma, in Coq.ZArith.Zminmax]
Z.plus_max_distr_r [lemma, in Coq.ZArith.Zminmax]
Z.pos_min [lemma, in Coq.ZArith.Zminmax]
Z.pos_max [lemma, in Coq.ZArith.Zminmax]
Z.pos_min_1 [lemma, in Coq.ZArith.Zminmax]
Z.pos_max_1 [lemma, in Coq.ZArith.Zminmax]
Z.pred_max_distr [lemma, in Coq.ZArith.Zminmax]
Z.pred_min_distr [lemma, in Coq.ZArith.Zminmax]
Z.succ_max_distr [lemma, in Coq.ZArith.Zminmax]
Z.succ_min_distr [lemma, in Coq.ZArith.Zminmax]
Z0 [constructor, in Coq.ZArith.BinInt]
Z2P [definition, in Coq.QArith.Qreduction]
Z2P_correct2 [lemma, in Coq.QArith.Qreduction]
Z2P_correct [lemma, 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 (19028 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 (451 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 (358 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 (101 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 (8297 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 (399 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 (754 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 (636 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 (404 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 (238 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 (3488 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 (612 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 (625 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 (2230 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 (435 entries)