proposition: Lemma Qpos_mult_le_compat : forall (a b : Qpos) (c d : Q), proj1_sig a <= c -> proj1_sig b <= d -> proj1_sig a * proj1_sig b <= c * d.
proof: Proof. intros. apply (Qle_trans _ (c * proj1_sig b)). apply Qmult_le_compat_r. exact H. apply Qpos_nonneg. rewrite Qmult_comm. rewrite (Qmult_comm c). apply Qmult_le_compat_r. exact H0. apply (Qle_trans _ (proj1_sig a)). apply Qpos_nonneg. exact H. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder