`{IsApart A} `{Alt : Lt A} `{is_mere_relation A lt} `{Apart B} `{Blt : Lt B} (f : A -> B) `{!IsStrongInjective f} `{!PseudoOrder Blt} : (forall x y, x < y <-> f x < f y) -> PseudoOrder Alt. Proof. pose proof (strong_injective_mor f). intros P. split; try apply _. - intros x y E. apply (pseudo_order_antisym (f x) (f y)). split; apply P,E. - intros x y E z. apply P in E. apply (merely_destruct (cotransitive E (f z))); intros [?|?];apply tr; [left | right]; apply P;trivial. - intros x y; split; intros E. + apply (strong_injective f) in E. apply apart_iff_total_lt in E. destruct E; [left | right]; apply P;trivial. + apply (strong_extensionality f). apply apart_iff_total_lt. destruct E; [left | right]; apply P;trivial. Qed.
Require Import