(f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsStrongInjective f} : (forall x y, x < y <-> f x < f y) -> PseudoSemiRingOrder R2lt. Proof. intros P. pose proof (projected_pseudo_order f P). pose proof (projected_strict_ring_order f P). apply from_pseudo_ring_order; try apply _. pose proof (@pseudo_order_apart R1 H0 R1lt pseudo_srorder_strict : IsApart R1). pose proof (pseudo_order_apart : IsApart R2). pose proof (strong_injective_mor f). repeat (split; try apply _). intros x₁ y₁ x₂ y₂ E. apply (strong_injective f) in E. rewrite 2!(preserves_mult (f:=f)) in E. apply (merely_destruct (strong_binary_extensionality (.*.) _ _ _ _ E)); intros [?|?];apply tr; [left | right]; apply (strong_extensionality f); trivial. Qed.
Require Import