Library Coq.Arith.Max
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')
end.
Lemma max_SS : forall n m, S (max n m) = max (S n) (S m).
Theorem max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
Lemma max_comm : forall n m, max n m = max m n.