Numbers: properties of min/max with respect to 0,S,P,add,sub,mul

 With these properties, we can kill Arith/MinMax, NArith/Nminmax,
 and leave ZArith/Zminmax as a compatibility file only. Now
 the instanciations NPeano.Nat, NBinary.N, ZBinary.Z, BigZ, BigN
 contains all theses facts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12718 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 10 deletions

diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 4703faace..e1599d943 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -7,16 +7,13 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
+(** THIS FILE IS DEPRECATED. Use [ZBinary.Z] instead. *)
 
-Require Import BinInt Zcompare Zorder Zminmax.
+Require Import BinInt Zcompare Zorder ZBinary.
 
 Open Local Scope Z_scope.
 
-(** [Zmin] is now [BinInt.Zmin]. Code that do things like
-  [unfold Zmin.Zmin] will have to be adapted, and neither
-  a [Definition] or a [Notation] here can help much. *)
-
+(** Definition [Zmin] is now [BinInt.Zmin]. *)
 
 (** * Characterization of the minimum on binary integer numbers *)
 
@@ -77,14 +74,24 @@ Notation Zmin_SS := Z.succ_min_distr (only parsing).
 
 Definition Zplus_min_distr_r :
  forall n m p, Zmin (n + p) (m + p) = Zmin n m + p
- := Z.plus_min_distr_r.
+ := Z.add_min_distr_r.
 
-Notation Zmin_plus := Z.plus_min_distr_r (only parsing).
+Notation Zmin_plus := Z.add_min_distr_r (only parsing).
 
 (** * Minimum and Zpos *)
 
-Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q)
- := Z.pos_min.
+Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
+Proof.
+ intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q).
+ destruct Pcompare; auto.
+Qed.
+
+Lemma Zpos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
+
+