proposition: Lemma projected_full_pseudo_ring_order (f : R2 → R1) `{!SemiRing_Morphism f} `{!StrongInjective f} : (∀ x y, x ≤ y ↔ f x ≤ f y) → (∀ x y, x < y ↔ f x < f y) → FullPseudoSemiRingOrder R2le R2lt.
proof: Proof. intros P1 P2. pose proof (projected_full_pseudo_order f P1 P2). pose proof (projected_pseudo_ring_order f P2). split; try apply _. apply le_iff_not_lt_flip. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings