`{!StrictlyOrderPreserving (f : A -> B)} : OrderReflecting f. Proof. intros x y E1. apply le_iff_not_lt_flip;apply le_iff_not_lt_flip in E1. intros E2. apply E1. apply (strictly_order_preserving f). trivial. Qed.
Require Import