proposition: Lemma full_pseudo_order_preserving `{!StrictlyOrderReflecting (f : A → B)} : OrderPreserving f.
proof: Proof. pose proof (strict_order_morphism_mor f). repeat (split; try apply _). intros x y. rewrite !le_iff_not_lt_flip. intros E1 E2. apply E1. now apply (strictly_order_reflecting f). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.orders MathClasses.theory.setoids MathClasses.theory.strong_setoids