Zmult_pos' : forall x y : Z, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y). Proof. unfold PropHolds. apply (Z_ind2 (fun _ _ => _ -> _ -> _)). intros [pa na] [pb nb]. rewrite !Zlt_def;unfold PairT.Tlt;simpl. rewrite !plus_0_l,!plus_0_r. intros E1 E2. destruct (decompose_lt E1) as [a [Ea1 Ea2]], (decompose_lt E2) as [b [Eb1 Eb2]]. rewrite Ea2, Eb2. apply compose_lt with (a * b). - apply pos_mult_compat;trivial. - ring_with_nat. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.