`{IsSemiCRing R2} `{R2le : Le R2} `{is_mere_relation R2 R2le} (f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsInjective f} : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall x y : R2, x ≤ y -> exists z, y = x + z) -> SemiRingOrder R2le. Proof. intros P. pose proof (projected_partial_order f P). repeat (split; try apply _). - assumption. - red;intros. apply P. rewrite 2!(preserves_plus (f:=f)). apply (order_preserving _), P. trivial. - red;intros. apply P. apply (order_reflecting (f z +)). rewrite <-2!preserves_plus. apply P. trivial. - intros. apply P. rewrite preserves_mult, preserves_0. apply nonneg_mult_compat; rewrite <-(preserves_0 (f:=f)); apply P;trivial. Qed.
Require Import