proposition: Lemma projected_full_pseudo_ring_order (f : R2 -> R1) `{!IsSemiRingPreserving f} `{!IsStrongInjective f} : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall 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: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings