proposition: Lemma min_max_antimonotone f : Proper (le ==> flip le) f -> forall x y, min (f x) (f y) = f (max x y).
proof: Proof. intros; apply min_max_antimono; auto. congruence. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics