diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-13 19:46:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-13 19:46:31 +0000 |
| commit | 411a23ee7b6ceacf04a343e6523c16d430bd2af2 (patch) | |
| tree | e88ab6d4fb392117a6b0b0a0d7323c27f9dce22e /theories/ZArith/Znumtheory.v | |
| parent | b99396f1ee52d285f4dca9cecc6e89b06105448f (diff) | |
typo
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index b6ade8fd3..5c0ed2ec0 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -697,7 +697,7 @@ destruct a; unfold Zmod; simpl; intros; auto; destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto. Qed. -Lemma Zggcd_gcdn : forall a b, fst (Zggcd a b) = Zgcd a b. +Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. Proof. intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto. Qed. |