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