Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358.

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

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index b7911181f..07eca7765 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -67,14 +67,18 @@ Proof.
   intros; apply Zmax_case_strong; auto with zarith.
 Qed.
 
+(* begin hide *)
 Notation Zmax1 := Zle_max_l (only parsing).
+(* end hide *)
 
 Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.
 Proof.
   intros; apply Zmax_case_strong; auto with zarith.
 Qed.
 
+(* begin hide *)
 Notation Zmax2 := Zle_max_r (only parsing).
+(* end hide *)
 
 Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.
 Proof.
@@ -86,6 +90,18 @@ Proof.
   intros; apply Zmax_case; assumption.
 Qed.
 
+(** * Compatibility with order *)
+
+Lemma Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p.
+Proof.
+  intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl.
+Qed.
+
+Lemma Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m.
+Proof.
+  intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl.
+Qed.
+
 (** * Semi-lattice properties of max *)
 
 Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.