Z_full_pseudo_srorder@{} : FullPseudoSemiRingOrder Zle Zlt. Proof. pose proof Z_ring. first [apply from_full_pseudo_ring_order@{UN UN UN UN UN UN UN Ularge}| apply from_full_pseudo_ring_order]; try apply _. apply apartness.strong_binary_setoid_morphism_commutative. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.