summaryrefslogtreecommitdiff
path: root/theories/Arith/Max.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch)
tree591e9e512063e34099782e2518573f15ffeac003 /theories/Arith/Max.v
parentde0085539583f59dc7c4bf4e272e18711d565466 (diff)
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/Arith/Max.v')
-rw-r--r--theories/Arith/Max.v42
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).