From 2d6eb6f004cb6a424234ef8ace8f19341eb3e5f8 Mon Sep 17 00:00:00 2001
From: notin
Date: Mon, 26 Jun 2006 13:57:44 +0000
Subject: Ajout de Zgcd_spec (compat.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/Znumtheory.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index d61cc84bcc..05076ebd34 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -926,7 +926,12 @@ generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb));
 destruct 1; subst; auto.
 Qed.
 
-(** A version of [Zgcd] that doesn't use an explicit measure can be found 
-  in users's contribution [Orsay/QArith]. It is slightly more efficient after 
-  extraction, but cannot be used to compute within Coq. *)
+Theorem Zgcd_spec : forall x y : Z, {z : Z | Zis_gcd x y z /\ 0 <= z}.
+Proof.
+  intros x y; exists (Zgcd x y).
+  split; [apply Zgcd_is_gcd  | apply Zgcd_is_pos].
+Qed.
+
+
+
 
-- 
cgit v1.2.3