(f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsInjective f} : (forall x y, x ≤ y <-> f x ≤ f y) -> SemiRingOrder R2le. Proof. intros P. apply (projected_srorder f P). intros x y E. exists (-x + y). rewrite plus_assoc, plus_negate_r, plus_0_l. reflexivity. Qed.
Require Import