diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/ZArith/Zmin.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/ZArith/Zmin.v')
-rw-r--r-- | theories/ZArith/Zmin.v | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 37d78a74..bad40a32 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,9 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmin.v 9302 2006-10-27 21:21:17Z barras $ i*) +(*i $Id: Zmin.v 10028 2007-07-18 22:38:06Z letouzey $ i*) -(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. +(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. Further extensions by the Coq development team, with suggestions from Russell O'Connor (Radbout U., Nijmegen, The Netherlands). *) @@ -43,6 +43,14 @@ Proof. intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith. Qed. +Lemma Zmin_spec : forall x y:Z, + x <= y /\ Zmin x y = x \/ + x > y /\ Zmin x y = y. +Proof. + intros; unfold Zmin, Zle, Zgt. + destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate. +Qed. + (** * Greatest lower bound properties of min *) Lemma Zle_min_l : forall n m:Z, Zmin n m <= n. @@ -128,3 +136,11 @@ Proof. Qed. Notation Zmin_plus := Zplus_min_distr_r (only parsing). + +(** * Minimum and Zpos *) + +Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Proof. + intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto. +Qed. + |