Zmult_nonneg' : 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 !Zle_def;unfold PairT.Tle;simpl. rewrite !plus_0_l,!plus_0_r. intros E1 E2. destruct (decompose_le E1) as [a [Ea1 Ea2]], (decompose_le E2) as [b [Eb1 Eb2]]. rewrite Ea2, Eb2. apply compose_le with (a * b). - apply nonneg_mult_compat;trivial. - ring_with_nat. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.