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