proposition: Lemma projected_strict_order `{Alt : Lt A} `{is_mere_relation A lt} `{Blt : Lt B} (f : A -> B) `{!StrictOrder Blt} : (forall x y, x < y <-> f x < f y) -> StrictOrder Alt.
proof: Proof. intros P. split. - apply _. - intros x E. destruct (irreflexivity (<) (f x)). apply P. trivial. - intros x y z E1 E2. apply P. transitivity (f y); apply P;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.orders HoTT.Classes.theory.apartness