From 411a23ee7b6ceacf04a343e6523c16d430bd2af2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 13 May 2006 19:46:31 +0000 Subject: typo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8814 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Znumtheory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/ZArith') 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. -- cgit v1.2.3