proposition: Lemma projected_ring_order (f : R2 → R1) `{!SemiRing_Morphism f} `{!Injective f} : (∀ x y, x ≤ y ↔ f x ≤ f y) → SemiRingOrder R2le.
proof: Proof. intros P. apply (projected_srorder f P). intros x y E. exists (-x + y). now rewrite associativity, plus_negate_r, plus_0_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings