proposition: Lemma projected_pseudo_ring_order (f : R2 → R1) `{!SemiRing_Morphism f} `{!StrongInjective f} : (∀ x y, x < y ↔ f x < f y) → PseudoSemiRingOrder R2lt.
proof: Proof. intros P. pose proof (projected_pseudo_order f P). pose proof (projected_strict_ring_order f P). apply from_pseudo_ring_order; try apply _. pose proof (pseudo_order_setoid : StrongSetoid R1). pose proof (pseudo_order_setoid : StrongSetoid R2). pose proof (strong_injective_mor f). repeat (split; try apply _). intros x₁ y₁ x₂ y₂ E. apply (strong_injective f) in E. rewrite 2!preserves_mult in E. destruct (strong_binary_extensionality (.*.) _ _ _ _ E); [left | right]; now apply (strong_extensionality f). Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.orders.semirings