proposition: Lemma min_max_antimono f : Proper (eq==>eq) f -> Proper (le==>flip le) f -> forall x y, min (f x) (f y) == f (max x y).
proof: Proof. intros Eqf Lef x y. destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E; destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto. - assert (f y <= f x) by (apply Lef; order). order. - assert (f x <= f y) by (apply Lef; order). order. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics