diff options
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. |