diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /theories/ZArith/Znumtheory.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
-rw-r--r-- | theories/ZArith/Znumtheory.v | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 0f58f524..f69cf315 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -308,11 +308,11 @@ Section extended_euclid_algorithm. intros v3 Hv3; generalize Hv3; pattern v3. apply Zlt_0_rec. clear v3 Hv3; intros. - elim (Z_zerop x); intro. + destruct (Z_zerop x) as [Heq|Hneq]. apply Euclid_intro with (u := u1) (v := u2) (d := u3). assumption. apply H3. - rewrite a0; auto with zarith. + rewrite Heq; auto with zarith. set (q := u3 / x) in *. assert (Hq : 0 <= u3 - q * x < x). replace (u3 - q * x) with (u3 mod x). @@ -605,11 +605,10 @@ Qed. Lemma prime_rel_prime : forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. Proof. - simple induction 1; intros. - constructor; intuition. - elim (prime_divisors p H x H3); intuition; subst; auto with zarith. - absurd (p | a); auto with zarith. - absurd (p | a); intuition. + intros; constructor; intros; auto with zarith. + apply prime_divisors in H1; intuition; subst; auto with zarith. + - absurd (p | a); auto with zarith. + - absurd (p | a); intuition. Qed. Hint Resolve prime_rel_prime: zarith. |