diff options
Diffstat (limited to 'theories/Arith/Min.v')
| -rw-r--r-- | theories/Arith/Min.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index db14e74b..aa009963 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Min.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Min.v 9660 2007-02-19 11:36:30Z notin $ i*) Require Import Le. @@ -25,11 +25,28 @@ Fixpoint min n m {struct n} : nat := (** * Simplifications of [min] *) +Lemma min_0_l : forall n : nat, min 0 n = 0. +Proof. + trivial. +Qed. + +Lemma min_0_r : forall n : nat, min n 0 = 0. +Proof. + destruct n; trivial. +Qed. + Lemma min_SS : forall n m, S (min n m) = min (S n) (S m). Proof. auto with arith. Qed. +Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p. +Proof. + induction m; destruct n; destruct p; trivial. + simpl. + auto using (IHm n p). +Qed. + Lemma min_comm : forall n m, min n m = min m n. Proof. induction n; induction m; simpl in |- *; auto with arith. |