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