diff options
| -rw-r--r-- | theories/Arith/Max.v | 7 | ||||
| -rw-r--r-- | theories/Arith/Min.v | 17 |
2 files changed, 24 insertions, 0 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 9d534a2d3d..a3d658d0ca 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -30,6 +30,13 @@ Proof. auto with arith. Qed. +Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p. +Proof. + induction m; destruct n; destruct p; trivial. + simpl. + auto using IHm. +Qed. + Lemma max_comm : forall n m, max n m = max m n. Proof. induction n; induction m; simpl in |- *; auto with arith. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 4d40ebaedd..7654c856ce 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -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. |