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

1 files changed, 7 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.