Zle_plus_preserving_l@{} : forall z : Z, OrderPreserving ((+) z) := ltac:(first [exact Zle_plus_preserving_l'@{Ularge Ularge}| exact Zle_plus_preserving_l']).
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.