proposition: Lemma projected_total_order `{Ale : Le A} `{Ble : Le B} (f : A -> B) `{!TotalRelation Ble} : (forall x y, x ≤ y <-> f x ≤ f y) -> TotalRelation Ale.
proof: Proof. intros P x y. destruct (total (≤) (f x) (f y)); [left | right]; apply P;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness