proposition: Lemma from_strict_ring_order: StrictSemiRingOrder (<).
proof: Proof. repeat (split; try apply _). intros x y E. exists (- x + y). now rewrite associativity, plus_negate_r, plus_0_l. intros x y E. rewrite <-(plus_0_l x), <-(plus_0_l y), <-!(plus_negate_l z), <-!associativity. now apply (strictly_order_preserving _). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings