diff options
Diffstat (limited to 'theories/Arith/Min.v')
| -rw-r--r-- | theories/Arith/Min.v | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 38351817..db14e74b 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,73 +6,73 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Min.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*) -Require Import Arith. +Require Import Le. Open Local Scope nat_scope. Implicit Types m n : nat. -(** minimum of two natural numbers *) +(** * minimum of two natural numbers *) Fixpoint min n m {struct n} : nat := match n, m with - | O, _ => 0 - | S n', O => 0 - | S n', S m' => S (min n' m') + | O, _ => 0 + | S n', O => 0 + | S n', S m' => S (min n' m') end. -(** Simplifications of [min] *) +(** * Simplifications of [min] *) Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). Proof. -auto with arith. + auto with arith. Qed. Lemma min_comm : forall n m, min n m = min m n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. -(** [min] and [le] *) +(** * [min] and [le] *) Lemma min_l : forall n m, n <= m -> min n m = n. Proof. -induction n; induction m; simpl in |- *; auto with arith. + induction n; induction m; simpl in |- *; auto with arith. Qed. Lemma min_r : forall n m, m <= n -> min 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_min_l : forall n m, min n m <= n. 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_min_r : forall n m, min n m <= 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 min_l min_r le_min_l le_min_r: arith v62. -(** [min n m] is equal to [n] or [m] *) +(** * [min n m] is equal to [n] or [m] *) Lemma min_dec : forall n m, {min n m = n} + {min 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 min_case : forall n m (P:nat -> Type), P n -> P m -> P (min n m). Proof. -induction n; simpl in |- *; auto with arith. -induction m; intros; simpl in |- *; auto with arith. -pattern (min n m) in |- *; apply IHn; auto with arith. + induction n; simpl in |- *; auto with arith. + induction m; intros; simpl in |- *; auto with arith. + pattern (min n m) in |- *; apply IHn; auto with arith. Qed. Notation min_case2 := min_case (only parsing). |