Zmult_nonneg@{} : forall x y : Z, PropHolds (0 ≤ x) -> PropHolds (0 ≤ y) -> PropHolds (0 ≤ x * y) := ltac:(first [exact Zmult_nonneg'@{Ularge Ularge Ularge}| exact Zmult_nonneg']). Global Z_order@{} : SemiRingOrder Zle. Proof. pose proof Z_ring; apply rings.from_ring_order; apply _. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.