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