diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-26 13:57:44 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-26 13:57:44 +0000 |
| commit | 2d6eb6f004cb6a424234ef8ace8f19341eb3e5f8 (patch) | |
| tree | e83338e2f0eede0863a7832b558073c3352d49dc /theories/ZArith/Znumtheory.v | |
| parent | 776c325e9599cfe88e498df444aabc9aef75d465 (diff) | |
Ajout de Zgcd_spec (compat.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Znumtheory.v')
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index d61cc84bc..05076ebd3 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. + + + |