diff options
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 272 |
1 files changed, 153 insertions, 119 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 9be372a3..2a2751c9 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znumtheory.v 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -15,13 +15,13 @@ Require Import Zdiv. Require Import Wf_nat. Open Local Scope Z_scope. -(** This file contains some notions of number theory upon Z numbers: +(** This file contains some notions of number theory upon Z numbers: - a divisibility predicate [Zdivide] - a gcd predicate [gcd] - Euclid algorithm [euclid] - a relatively prime predicate [rel_prime] - a prime predicate [prime] - - an efficient [Zgcd] function + - an efficient [Zgcd] function *) (** * Divisibility *) @@ -171,7 +171,7 @@ Proof. rewrite H1 in H0; left; omega. rewrite H1 in H0; right; omega. Qed. - + Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) -> (a | c). Proof. intros a b c [d H1] [e H2]; exists (d * e); auto with zarith. @@ -201,19 +201,17 @@ Qed. (** [Zdivide] can be expressed using [Zmod]. *) -Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). +Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a). Proof. - intros a b H H0. - apply Zdivide_intro with (a / b). - pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). - rewrite H0; ring. + intros a b NZ EQ. + apply Zdivide_intro with (a/b). + rewrite (Z_div_mod_eq_full a b NZ) at 1. + rewrite EQ; ring. Qed. -Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. +Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0. Proof. - intros a b; simple destruct 2; intros; subst. - change (q * b) with (0 + q * b) in |- *. - rewrite Z_mod_plus; auto. + intros a b (c,->); apply Z_mod_mult. Qed. (** [Zdivide] is hence decidable *) @@ -222,7 +220,7 @@ Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}. Proof. intros a b; elim (Ztrichotomy_inf a 0). (* a<0 *) - intros H; elim H; intros. + intros H; elim H; intros. case (Z_eq_dec (b mod - a) 0). left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith. intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. @@ -236,7 +234,7 @@ Proof. intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. Qed. -Theorem Zdivide_Zdiv_eq: forall a b : Z, +Theorem Zdivide_Zdiv_eq: forall a b : Z, 0 < a -> (a | b) -> b = a * (b / a). Proof. intros a b Hb Hc. @@ -244,7 +242,7 @@ Proof. rewrite (Zdivide_mod b a); auto with zarith. Qed. -Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, +Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, 0 < a -> (a | b) -> (c * b)/a = c * (b / a). Proof. intros a b c H1 H2. @@ -252,7 +250,7 @@ Proof. rewrite Hz; rewrite Zmult_assoc. repeat rewrite Z_div_mult; auto with zarith. Qed. - + Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) -> (a | b). Proof. intros a b [x H]; subst b. @@ -260,7 +258,7 @@ Proof. exists (- x); ring. exists x; ring. Qed. - + Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) -> (Zabs a | b). Proof. intros a b [x H]; subst b. @@ -269,7 +267,7 @@ Proof. exists x; ring. Qed. -Theorem Zdivide_le: forall a b : Z, +Theorem Zdivide_le: forall a b : Z, 0 <= a -> 0 < b -> (a | b) -> a <= b. Proof. intros a b H1 H2 [q H3]; subst b. @@ -280,7 +278,7 @@ Proof. intros H4; subst q; omega. Qed. -Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, +Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . Proof. intros a b H1 H2 H3; split. @@ -307,7 +305,7 @@ Proof. rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. Qed. -Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> +Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> a mod b = c -> (b | a - c). Proof. intros a b c H H1; apply Zmod_divide; auto with zarith. @@ -317,7 +315,7 @@ Proof. subst; apply Z_mod_lt; auto with zarith. Qed. -Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> +Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> (b | a - c) -> a mod b = c. Proof. intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto. @@ -328,9 +326,9 @@ Proof. Qed. (** * Greatest common divisor (gcd). *) - -(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] - expressing that [d] is a gcd of [a] and [b]. + +(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] + expressing that [d] is a gcd of [a] and [b]. (We show later that the [gcd] is actually unique if we discard its sign.) *) Inductive Zis_gcd (a b d:Z) : Prop := @@ -379,8 +377,8 @@ Proof. Qed. Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. - -Theorem Zis_gcd_unique: forall a b c d : Z, + +Theorem Zis_gcd_unique: forall a b c d : Z, Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d). Proof. intros a b c d H1 H2. @@ -431,7 +429,7 @@ Section extended_euclid_algorithm. (** The recursive part of Euclid's algorithm uses well-founded recursion of non-negative integers. It maintains 6 integers [u1,u2,u3,v1,v2,v3] such that the following invariant holds: - [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. + [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. *) Lemma euclid_rec : @@ -455,8 +453,8 @@ Section extended_euclid_algorithm. replace (u3 - q * x) with (u3 mod x). apply Z_mod_lt; omega. assert (xpos : x > 0). omega. - generalize (Z_div_mod_eq u3 x xpos). - unfold q in |- *. + generalize (Z_div_mod_eq u3 x xpos). + unfold q in |- *. intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)). tauto. @@ -531,7 +529,7 @@ Proof. rewrite H6; rewrite H7; ring. ring. Qed. - + (** * Relative primality *) @@ -612,16 +610,16 @@ Proof. intros a b g; intros. assert (g <> 0). intro. - elim H1; intros. + elim H1; intros. elim H4; intros. rewrite H2 in H6; subst b; omega. unfold rel_prime in |- *. destruct H1. destruct H1 as (a',H1). destruct H3 as (b',H3). - replace (a/g) with a'; + replace (a/g) with a'; [|rewrite H1; rewrite Z_div_mult; auto with zarith]. - replace (b/g) with b'; + replace (b/g) with b'; [|rewrite H3; rewrite Z_div_mult; auto with zarith]. constructor. exists a'; auto with zarith. @@ -643,7 +641,7 @@ Proof. red; apply Zis_gcd_sym; auto with zarith. Qed. -Theorem rel_prime_div: forall p q r, +Theorem rel_prime_div: forall p q r, rel_prime p q -> (r | p) -> rel_prime r q. Proof. intros p q r H (u, H1); subst. @@ -670,7 +668,7 @@ Proof. exists 1; auto with zarith. Qed. -Theorem rel_prime_mod: forall p q, 0 < q -> +Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q. Proof. intros p q H H0. @@ -683,7 +681,7 @@ Proof. pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. Qed. -Theorem rel_prime_mod_rev: forall p q, 0 < q -> +Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. Proof. intros p q H H0. @@ -715,7 +713,7 @@ Proof. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ]. - generalize H3. + generalize H3. pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; apply Zabs_ind; intros; omega. intuition idtac. @@ -785,7 +783,7 @@ Proof. intros H1; absurd (1 < 1); auto with zarith. inversion H1; auto. Qed. - + Lemma prime_2: prime 2. Proof. apply prime_intro; auto with zarith. @@ -795,7 +793,7 @@ Proof. subst n; red; auto with zarith. apply Zis_gcd_intro; auto with zarith. Qed. - + Theorem prime_3: prime 3. Proof. apply prime_intro; auto with zarith. @@ -812,7 +810,7 @@ Proof. subst n; red; auto with zarith. apply Zis_gcd_intro; auto with zarith. Qed. - + Theorem prime_ge_2: forall p, prime p -> 2 <= p. Proof. intros p Hp; inversion Hp; auto with zarith. @@ -820,7 +818,7 @@ Qed. Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). -Theorem prime_alt: +Theorem prime_alt: forall p, prime' p <-> prime p. Proof. split; destruct 1; intros. @@ -848,7 +846,7 @@ Proof. apply Zis_gcd_intro; auto with zarith. apply H0; auto with zarith. Qed. - + Theorem square_not_prime: forall a, ~ prime (a * a). Proof. intros a Ha. @@ -864,10 +862,10 @@ Proof. exists b; auto. Qed. -Theorem prime_div_prime: forall p q, +Theorem prime_div_prime: forall p q, prime p -> prime q -> (p | q) -> p = q. Proof. - intros p q H H1 H2; + intros p q H H1 H2; assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. @@ -878,10 +876,10 @@ Proof. Qed. -(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose +(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose here a binary version of [Zgcd], faster and executable within Coq. - Algorithm: + Algorithm: gcd 0 b = b gcd a 0 = a @@ -889,23 +887,23 @@ Qed. gcd (2a+1) (2b) = gcd (2a+1) b gcd (2a) (2b+1) = gcd a (2b+1) gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1) - or gcd (a-b) (2*b+1), depending on whether a<b -*) + or gcd (a-b) (2*b+1), depending on whether a<b +*) Open Scope positive_scope. -Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := - match n with +Fixpoint Pgcdn (n: nat) (a b : positive) : positive := + match n with | O => 1 - | S n => - match a,b with - | xH, _ => 1 + | S n => + match a,b with + | xH, _ => 1 | _, xH => 1 | xO a, xO b => xO (Pgcdn n a b) | a, xO b => Pgcdn n a b | xO a, b => Pgcdn n a b - | xI a', xI b' => - match Pcompare a' b' Eq with + | xI a', xI b' => + match Pcompare a' b' Eq with | Eq => a | Lt => Pgcdn n (b'-a') a | Gt => Pgcdn n (a'-b') b @@ -919,7 +917,7 @@ Close Scope positive_scope. Definition Zgcd (a b : Z) : Z := match a,b with - | Z0, _ => Zabs b + | Z0, _ => Zabs b | _, Z0 => Zabs a | Zpos a, Zpos b => Zpos (Pgcd a b) | Zpos a, Zneg b => Zpos (Pgcd a b) @@ -932,8 +930,8 @@ Proof. unfold Zgcd; destruct a; destruct b; auto with zarith. Qed. -Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> - Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. +Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> + Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. Proof. intros. destruct H. @@ -951,7 +949,7 @@ Proof. omega. Qed. -Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> +Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)). Proof. intro n; pattern n; apply lt_wf_ind; clear n; intros. @@ -977,7 +975,7 @@ Proof. rewrite (Zpos_minus_morphism _ _ H1). assert (0 < Zpos a) by (compute; auto). omega. - omega. + omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. rewrite Zpos_minus_morphism; auto. omega. @@ -995,7 +993,7 @@ Proof. assert (0 < Zpos b) by (compute; auto). omega. rewrite ZC4; rewrite H1; auto. - omega. + omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. rewrite Zpos_minus_morphism; auto. omega. @@ -1062,7 +1060,7 @@ Proof. split; [apply Zgcd_is_gcd | apply Zgcd_is_pos]. Qed. -Theorem Zdivide_Zgcd: forall p q r : Z, +Theorem Zdivide_Zgcd: forall p q r : Z, (p | q) -> (p | r) -> (p | Zgcd q r). Proof. intros p q r H1 H2. @@ -1071,7 +1069,7 @@ Proof. inversion_clear H3; auto. Qed. -Theorem Zis_gcd_gcd: forall a b c : Z, +Theorem Zis_gcd_gcd: forall a b c : Z, 0 <= c -> Zis_gcd a b c -> Zgcd a b = c. Proof. intros a b c H1 H2. @@ -1103,7 +1101,7 @@ Proof. rewrite H1; ring. Qed. -Theorem Zgcd_div_swap0 : forall a b : Z, +Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Zgcd a b -> 0 < b -> (a / Zgcd a b) * b = a * (b/Zgcd a b). @@ -1116,7 +1114,7 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Theorem Zgcd_div_swap : forall a b c : Z, +Theorem Zgcd_div_swap : forall a b c : Z, 0 < Zgcd a b -> 0 < b -> (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b). @@ -1131,7 +1129,43 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Theorem Zgcd_1_rel_prime : forall a b, +Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a. +Proof. + intros. + apply Zis_gcd_gcd. + apply Zgcd_is_pos. + apply Zis_gcd_sym. + apply Zgcd_is_gcd. +Qed. + +Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). +Proof. + intros. + apply Zis_gcd_gcd. + apply Zgcd_is_pos. + destruct (Zgcd_is_gcd a b). + destruct (Zgcd_is_gcd b c). + destruct (Zgcd_is_gcd a (Zgcd b c)). + constructor; eauto using Zdivide_trans. +Qed. + +Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zgcd_1 : forall a, Zgcd a 1 = 1. +Proof. + intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1. +Qed. +Hint Resolve Zgcd_0 Zgcd_1 : zarith. + +Theorem Zgcd_1_rel_prime : forall a b, Zgcd a b = 1 <-> rel_prime a b. Proof. unfold rel_prime; split; intro H. @@ -1142,7 +1176,7 @@ Proof. generalize (Zgcd_is_pos a b); auto with zarith. Qed. -Definition rel_prime_dec: forall a b, +Definition rel_prime_dec: forall a b, { rel_prime a b }+{ ~ rel_prime a b }. Proof. intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1. @@ -1156,10 +1190,10 @@ Definition prime_dec_aux: { exists n, 1 < n < m /\ ~ rel_prime n p }. Proof. intros p m. - case (Z_lt_dec 1 m); intros H1; - [ | left; intros; elimtype False; omega ]. + case (Z_lt_dec 1 m); intros H1; + [ | left; intros; exfalso; omega ]. pattern m; apply natlike_rec; auto with zarith. - left; intros; elimtype False; omega. + left; intros; exfalso; omega. intros x Hx IH; destruct IH as [F|E]. destruct (rel_prime_dec x p) as [Y|N]. left; intros n [HH1 HH2]. @@ -1221,34 +1255,34 @@ Qed. Open Scope positive_scope. -Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := - match n with +Fixpoint Pggcdn (n: nat) (a b : positive) : (positive*(positive*positive)) := + match n with | O => (1,(a,b)) - | S n => - match a,b with - | xH, b => (1,(1,b)) + | S n => + match a,b with + | xH, b => (1,(1,b)) | a, xH => (1,(a,1)) - | xO a, xO b => - let (g,p) := Pggcdn n a b in + | xO a, xO b => + let (g,p) := Pggcdn n a b in (xO g,p) - | a, xO b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in + | a, xO b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in (g,(aa, xO bb)) - | xO a, b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in + | xO a, b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in (g,(xO aa, bb)) - | xI a', xI b' => - match Pcompare a' b' Eq with + | xI a', xI b' => + match Pcompare a' b' Eq with | Eq => (a,(1,1)) - | Lt => - let (g,p) := Pggcdn n (b'-a') a in - let (ba,aa) := p in + | Lt => + let (g,p) := Pggcdn n (b'-a') a in + let (ba,aa) := p in (g,(aa, aa + xO ba)) - | Gt => - let (g,p) := Pggcdn n (a'-b') b in - let (ab,bb) := p in + | Gt => + let (g,p) := Pggcdn n (a'-b') b in + let (ab,bb) := p in (g,(bb+xO ab, bb)) end end @@ -1260,28 +1294,28 @@ Open Scope Z_scope. Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with - | Z0, _ => (Zabs b,(0, Zsgn b)) + | Z0, _ => (Zabs b,(0, Zsgn b)) | _, Z0 => (Zabs a,(Zsgn a, 0)) - | Zpos a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zpos a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zpos aa, Zpos bb)) - | Zpos a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zpos a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zpos aa, Zneg bb)) - | Zneg a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zneg a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zneg aa, Zpos bb)) | Zneg a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zneg aa, Zneg bb)) end. -Lemma Pggcdn_gcdn : forall n a b, +Lemma Pggcdn_gcdn : forall n a b, fst (Pggcdn n a b) = Pgcdn n a b. Proof. induction n. @@ -1302,15 +1336,15 @@ Qed. Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. Proof. - destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; + destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto. Qed. Open Scope positive_scope. -Lemma Pggcdn_correct_divisors : forall n a b, - let (g,p) := Pggcdn n a b in - let (aa,bb):=p in +Lemma Pggcdn_correct_divisors : forall n a b, + let (g,p) := Pggcdn n a b in + let (aa,bb):=p in (a=g*aa) /\ (b=g*bb). Proof. induction n. @@ -1337,7 +1371,7 @@ Proof. rewrite <- H1; rewrite <- H0. simpl; f_equal; symmetry. apply Pplus_minus; auto. - (* Then... *) + (* Then... *) generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl. intros (H0,H1); split; auto. rewrite Pmult_xO_permute_r; rewrite H1; auto. @@ -1348,9 +1382,9 @@ Proof. intros (H0,H1); split; subst; auto. Qed. -Lemma Pggcd_correct_divisors : forall a b, - let (g,p) := Pggcd a b in - let (aa,bb):=p in +Lemma Pggcd_correct_divisors : forall a b, + let (g,p) := Pggcd a b in + let (aa,bb):=p in (a=g*aa) /\ (b=g*bb). Proof. intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). @@ -1358,17 +1392,17 @@ Qed. Close Scope positive_scope. -Lemma Zggcd_correct_divisors : forall a b, - let (g,p) := Zggcd a b in - let (aa,bb):=p in +Lemma Zggcd_correct_divisors : forall a b, + let (g,p) := Zggcd a b in + let (aa,bb):=p in (a=g*aa) /\ (b=g*bb). Proof. - destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; - generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); + destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; + generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); destruct 1; subst; auto. Qed. -Theorem Zggcd_opp: forall x y, +Theorem Zggcd_opp: forall x y, Zggcd (-x) y = let (p1,p) := Zggcd x y in let (p2,p3) := p in (p1,(-p2,p3)). |