(f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsStrongInjective f} : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall x y, x < y <-> f x < f y) -> FullPseudoSemiRingOrder R2le R2lt. Proof. intros P1 P2. pose proof (projected_full_pseudo_order f P1 P2). pose proof (projected_pseudo_ring_order f P2). split; try apply _. apply le_iff_not_lt_flip. Qed.
Require Import