Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 21 insertions, 21 deletions

diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 7f5c1148..e0222e41 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Max.v 8642 2006-03-17 10:09:02Z notin $ i*)
+(*i $Id: Max.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Arith.
 
@@ -14,66 +14,66 @@ Open Local Scope nat_scope.
 
 Implicit Types m n : nat.
 
-(** maximum of two natural numbers *)
+(** * 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')
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
   end.
 
-(** Simplifications of [max] *)
+(** * Simplifications of [max] *)
 
 Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
 Proof.
-auto with arith.
+  auto with arith.
 Qed.
 
 Lemma max_comm : forall n m, max n m = max m n.
 Proof.
-induction n; induction m; simpl in |- *; auto with arith.
+  induction n; induction m; simpl in |- *; auto with arith.
 Qed.
 
-(** [max] and [le] *)
+(** * [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.
+  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.
+  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.
+  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.
+  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] *)
+(** * [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.
+  induction n; induction m; simpl in |- *; auto with arith.
+  elim (IHn m); intro H; elim H; auto.
 Qed.
 
 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.
+  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.
 Qed.
 
 Notation max_case2 := max_case (only parsing).