1 files changed, 35 insertions, 77 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 5de2298d..3d7fe9fc 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,81 +6,39 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 11735 2009-01-02 17:22:31Z herbelin $ i*)
-
-Require Import Le.
-
-Open Local Scope nat_scope.
-
-Implicit Types m n : nat.
-
-(** * maximum of two natural numbers *)
-
-Fixpoint max n m {struct n} : nat :=
-  match n, m with
-    | O, _ => m
-    | S n', O => n
-    | S n', S m' => S (max n' m')
-  end.
-
-(** * Simplifications of [max] *)
-
-Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
-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.
-Qed.
-
-(** * [max] and [le] *)
-
-Lemma max_l : forall n m, m <= n -> max n m = n.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma max_r : forall n m, n <= m -> max n m = m.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_max_l : forall n m, n <= max n m.
-Proof.
-  induction n; intros; simpl in |- *; auto with arith.
-  elim m; intros; simpl in |- *; auto with arith.
-Qed.
-
-Lemma le_max_r : forall n m, m <= max n m.
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; simpl in |- *; auto with arith.
-Qed.
-Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
-
-
-(** * [max n m] is equal to [n] or [m] *)
-
-Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
-Proof.
-  induction n; induction m; simpl in |- *; auto with arith.
-  elim (IHn m); intro H; elim H; auto.
-Defined.
-
-Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
-Proof.
-  induction n; simpl in |- *; auto with arith.
-  induction m; intros; simpl in |- *; auto with arith.
-  pattern (max n m) in |- *; apply IHn; auto with arith.
-Defined.
-
+(*i $Id$ i*)
+
+(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
+
+Require Export MinMax.
+
+Local Open Scope nat_scope.
+Implicit Types m n p : nat.
+
+Notation max := MinMax.max (only parsing).
+
+Definition max_0_l := max_0_l.
+Definition max_0_r := max_0_r.
+Definition succ_max_distr := succ_max_distr.
+Definition plus_max_distr_l := plus_max_distr_l.
+Definition plus_max_distr_r := plus_max_distr_r.
+Definition max_case_strong := max_case_strong.
+Definition max_spec := max_spec.
+Definition max_dec := max_dec.
+Definition max_case := max_case.
+Definition max_idempotent := max_id.
+Definition max_assoc := max_assoc.
+Definition max_comm := max_comm.
+Definition max_l := max_l.
+Definition max_r := max_r.
+Definition le_max_l := le_max_l.
+Definition le_max_r := le_max_r.
+Definition max_lub_l := max_lub_l.
+Definition max_lub_r := max_lub_r.
+Definition max_lub := max_lub.
+
+(* begin hide *)
+(* Compatibility *)
 Notation max_case2 := max_case (only parsing).
+Notation max_SS := succ_max_distr (only parsing).
+(* end hide *)