proposition: Lemma Qmult_le_compat_l (x y z : Q): x <= y -> 0 <= z -> z * x <= z * y.
proof: Proof. do 2 rewrite (Qmult_comm z). apply Qmult_le_compat_r. 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