proposition: Lemma projected_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsInjective f} : (forall 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). rewrite plus_assoc, plus_negate_r, plus_0_l. reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings