`{IsHSet A} {Ale : Le A} `{is_mere_relation A Ale} `{Ble : Le B} (f : A -> B) `{!IsInjective f} `{!PartialOrder Ble} : (forall x y, x ≤ y <-> f x ≤ f y) -> PartialOrder Ale. Proof. intros P. repeat split. - apply _. - apply _. - intros x. apply P. apply reflexivity. - intros x y z E1 E2. apply P. transitivity (f y); apply P;trivial. - intros x y E1 E2. apply (injective f). apply (antisymmetry (≤)); apply P;trivial. Qed.
Require Import