Zmult_pos@{} : forall x y : Z, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y) := ltac:(first [exact Zmult_pos'@{Ularge Ularge Ularge}| exact Zmult_pos'@{}]). Global Z_strict_srorder : StrictSemiRingOrder Zlt. Proof. pose proof Z_ring; apply from_strict_ring_order; apply _. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.