diff options
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index e77475e0..9be372a3 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 10295 2007-11-06 22:46:21Z letouzey $ i*) +(*i $Id: Znumtheory.v 11282 2008-07-28 11:51:53Z msozeau $ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -522,7 +522,7 @@ Lemma Zis_gcd_mult : forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). Proof. intros a b c d; simple induction 1; constructor; intuition. - elim (Zis_gcd_bezout a b d H); intros. + elim (Zis_gcd_bezout a b d H). intros. elim H3; intros. elim H4; intros. apply Zdivide_intro with (u * q + v * q0). |