proposition: Lemma from_full_pseudo_ring_order: FullPseudoSemiRingOrder (≤) (<).
proof: Proof. split. - apply _. - apply from_pseudo_ring_order;trivial. - apply le_iff_not_lt_flip;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.rings HoTT.Classes.orders.semirings