proposition: Lemma Qmult_lt_0_compat (x y: Q): 0 < x -> 0 < y -> 0 < x * y.
proof: Proof. destruct x, y. unfold Qlt. simpl. repeat rewrite Zmult_1_r. apply Zmult_lt_0_compat. Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List