`{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. 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.
Require Import