proposition: Lemma Qmult_le_compat: forall x y x' y' : Q, 0 <= x <= x' -> 0 <= y <= y' -> x * y <= x' * y'.
proof: Proof. intros. apply Qle_trans with (x * y'). do 2 rewrite (Qmult_comm x). apply Qmult_le_compat_r; intuition. apply Qmult_le_compat_r. intuition. apply Qle_trans with y; intuition. Qed.
imports: Coq.QArith.Qabs CoRN.model.ordfields.Qordfield CoRN.model.structures.Qpossec Coq.QArith.Qminmax Coq.setoid_ring.Ring Coq.Program.Program