proposition: Lemma min_unicity_ext f : (forall n m, (n < m /\ f n m == n) \/ (m <= n /\ f n m == m)) -> (forall n m, f n m == min n m).
proof: Proof. intros. apply min_unicity; auto. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics