proposition: Lemma Zmult_pos' : forall x y : Z, PropHolds (0 < x) -> PropHolds (0 < y) -> PropHolds (0 < x * y).
proof: 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.
imports: HoTT.HIT.quotient HoTT.TruncType HoTT.Basics.Trunc HoTT.Classes.implementations.peano_naturals HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.integers HoTT.Classes.theory.rings HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.orders.sum HoTT.Classes.orders.rings HoTT.Classes.tactics.ring_tac HoTT.Classes.theory.naturals