Imported Upstream version 8.5~beta1+dfsg

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.