diff options
Diffstat (limited to 'theories/Arith/Max.v')
| -rw-r--r-- | theories/Arith/Max.v | 42 |
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). |