diff options
Diffstat (limited to 'theories/ZArith')
| -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 594c07356..c741f4bc4 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -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). |