Ajouts de lemmes dans Min et Max

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

2 files changed, 24 insertions, 0 deletions

diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 9d534a2d3..a3d658d0c 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -30,6 +30,13 @@ Proof.
   auto with arith.
 Qed.
 
+Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
+Proof.
+  induction m; destruct n; destruct p; trivial.
+  simpl.
+  auto using IHm.
+Qed.
+
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
   induction n; induction m; simpl in |- *; auto with arith.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 4d40ebaed..7654c856c 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -25,11 +25,28 @@ Fixpoint min n m {struct n} : nat :=
 
 (** * Simplifications of [min] *)
 
+Lemma min_0_l : forall n : nat, min 0 n = 0.
+Proof.
+  trivial. 
+Qed.
+
+Lemma min_0_r : forall n : nat, min n 0 = 0.
+Proof.
+  destruct n; trivial.
+Qed.
+
 Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
 Proof.
   auto with arith.
 Qed.
 
+Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
+Proof.
+  induction m; destruct n; destruct p; trivial.
+  simpl.
+  auto using (IHm n p).
+Qed.
+
 Lemma min_comm : forall n m, min n m = min m n.
 Proof.
   induction n; induction m; simpl in |- *; auto with arith.