1 files changed, 9 insertions, 2 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index e0222e41..95af67f8 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Max.v 9883 2007-06-07 18:44:59Z letouzey $ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
@@ -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.