diff options
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 62 |
1 files changed, 31 insertions, 31 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 814b67322..00019b1a3 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -25,20 +25,20 @@ Open Scope Z_scope. - properties of the efficient [Z.gcd] function *) -Notation Zgcd := Z.gcd (only parsing). -Notation Zggcd := Z.ggcd (only parsing). -Notation Zggcd_gcd := Z.ggcd_gcd (only parsing). -Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (only parsing). -Notation Zgcd_divide_l := Z.gcd_divide_l (only parsing). -Notation Zgcd_divide_r := Z.gcd_divide_r (only parsing). -Notation Zgcd_greatest := Z.gcd_greatest (only parsing). -Notation Zgcd_nonneg := Z.gcd_nonneg (only parsing). -Notation Zggcd_opp := Z.ggcd_opp (only parsing). +Notation Zgcd := Z.gcd (compat "8.3"). +Notation Zggcd := Z.ggcd (compat "8.3"). +Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.3"). +Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.3"). +Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.3"). +Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.3"). +Notation Zgcd_greatest := Z.gcd_greatest (compat "8.3"). +Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.3"). +Notation Zggcd_opp := Z.ggcd_opp (compat "8.3"). (** The former specialized inductive predicate [Zdivide] is now a generic existential predicate. *) -Notation Zdivide := Z.divide (only parsing). +Notation Zdivide := Z.divide (compat "8.3"). (** Its former constructor is now a pseudo-constructor. *) @@ -46,17 +46,17 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H. (** Results concerning divisibility*) -Notation Zdivide_refl := Z.divide_refl (only parsing). -Notation Zone_divide := Z.divide_1_l (only parsing). -Notation Zdivide_0 := Z.divide_0_r (only parsing). -Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing). -Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (only parsing). -Notation Zdivide_plus_r := Z.divide_add_r (only parsing). -Notation Zdivide_minus_l := Z.divide_sub_r (only parsing). -Notation Zdivide_mult_l := Z.divide_mul_l (only parsing). -Notation Zdivide_mult_r := Z.divide_mul_r (only parsing). -Notation Zdivide_factor_r := Z.divide_factor_l (only parsing). -Notation Zdivide_factor_l := Z.divide_factor_r (only parsing). +Notation Zdivide_refl := Z.divide_refl (compat "8.3"). +Notation Zone_divide := Z.divide_1_l (compat "8.3"). +Notation Zdivide_0 := Z.divide_0_r (compat "8.3"). +Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (compat "8.3"). +Notation Zmult_divide_compat_r := Z.mul_divide_mono_r (compat "8.3"). +Notation Zdivide_plus_r := Z.divide_add_r (compat "8.3"). +Notation Zdivide_minus_l := Z.divide_sub_r (compat "8.3"). +Notation Zdivide_mult_l := Z.divide_mul_l (compat "8.3"). +Notation Zdivide_mult_r := Z.divide_mul_r (compat "8.3"). +Notation Zdivide_factor_r := Z.divide_factor_l (compat "8.3"). +Notation Zdivide_factor_l := Z.divide_factor_r (compat "8.3"). Lemma Zdivide_opp_r a b : (a | b) -> (a | - b). Proof. apply Z.divide_opp_r. Qed. @@ -91,12 +91,12 @@ Qed. (** Only [1] and [-1] divide [1]. *) -Notation Zdivide_1 := Z.divide_1_r (only parsing). +Notation Zdivide_1 := Z.divide_1_r (compat "8.3"). (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) -Notation Zdivide_antisym := Z.divide_antisym (only parsing). -Notation Zdivide_trans := Z.divide_trans (only parsing). +Notation Zdivide_antisym := Z.divide_antisym (compat "8.3"). +Notation Zdivide_trans := Z.divide_trans (compat "8.3"). (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) @@ -742,7 +742,7 @@ Qed. (** we now prove that [Z.gcd] is indeed a gcd in the sense of [Zis_gcd]. *) -Notation Zgcd_is_pos := Z.gcd_nonneg (only parsing). +Notation Zgcd_is_pos := Z.gcd_nonneg (compat "8.3"). Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Z.gcd a b). Proof. @@ -775,8 +775,8 @@ Proof. subst. now case (Z.gcd a b). Qed. -Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (only parsing). -Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (only parsing). +Notation Zgcd_inv_0_l := Z.gcd_eq_0_l (compat "8.3"). +Notation Zgcd_inv_0_r := Z.gcd_eq_0_r (compat "8.3"). Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Z.gcd a b -> @@ -806,16 +806,16 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Notation Zgcd_comm := Z.gcd_comm (only parsing). +Notation Zgcd_comm := Z.gcd_comm (compat "8.3"). Lemma Zgcd_ass a b c : Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). Proof. symmetry. apply Z.gcd_assoc. Qed. -Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing). -Notation Zgcd_0 := Z.gcd_0_r (only parsing). -Notation Zgcd_1 := Z.gcd_1_r (only parsing). +Notation Zgcd_Zabs := Z.gcd_abs_l (compat "8.3"). +Notation Zgcd_0 := Z.gcd_0_r (compat "8.3"). +Notation Zgcd_1 := Z.gcd_1_r (compat "8.3"). Hint Resolve Zgcd_0 Zgcd_1 : zarith. |