diff options
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. |