proposition: Lemma projected_strict_ring_order (f : R2 → R1) `{!SemiRing_Morphism f} : (∀ x y, x < y ↔ f x < f y) → StrictSemiRingOrder R2lt.
proof: Proof. intros P. pose proof (projected_strict_setoid_order f P). apply from_strict_ring_order. repeat (split; try apply _). intros x y E. apply P. rewrite 2!preserves_plus. now apply (strictly_order_preserving _), P. intros x y E1 E2. apply P. rewrite preserves_mult, preserves_0. now apply pos_mult_compat; rewrite <-(preserves_0 (f:=f)); apply P. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings