proposition: Lemma projected_strict_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f} : (forall x y, x < y <-> f x < f y) -> StrictSemiRingOrder R2lt.
proof: Proof. intros P. pose proof (projected_strict_order f P). apply from_strict_ring_order. - intros z x y E. apply P. rewrite 2!(preserves_plus (f:=f)). apply (strictly_order_preserving _), P. trivial. - intros x y E1 E2. apply P. rewrite preserves_mult, preserves_0. apply pos_mult_compat; rewrite <-(preserves_0 (f:=f)); apply P; trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings