proposition: Lemma Qmult_pos_neg (x y : Q) : 0 < x -> y < 0 -> x * y < 0.
proof: Proof. intros H1 H2. rewrite Qmult_comm. now apply Qmult_neg_pos. 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