Library Coq.Arith.Min
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')
end.
Lemma min_0_l : forall n : nat, min 0 n = 0.
Lemma min_0_r : forall n : nat, min n 0 = 0.
Lemma min_SS : forall n m, S (min n m) = min (S n) (S m).
Lemma min_assoc : forall m n p : nat, min m (min n p) = min (min m n) p.
Lemma min_comm : forall n m, min n m = min m n.