Z_full_psorder@{} : FullPseudoOrder Zle Zlt := ltac:(first [exact Z_full_psorder'@{Ularge Ularge Ularge Ularge Ularge Ularge Ularge Ularge Ularge}| exact Z_full_psorder'@{Ularge Ularge Ularge Ularge Ularge Ularge Ularge Ularge Ularge Ularge}| exact Z_full_psorder'@{}]).
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.