proposition: Lemma max_spec n m : (n < m /\ max n m == m) \/ (m <= n /\ max n m == n).
proof: Proof. destruct (lt_total n m); [left|right]. - split; auto. apply max_r. rewrite le_lteq; auto. - assert (m <= n) by (rewrite le_lteq; intuition auto with relations). split; auto. now apply max_l. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics