proposition: Lemma projected_partial_order `{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: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness