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