proposition: Lemma max_unicity n m p : ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m.
proof: Proof. assert (Hm := max_spec n m). destruct (lt_total n m); intuition; order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics