proposition: Lemma QboundAbs_upperBound_2 : forall (a b : Qpos) (c d : Q), (QboundAbs a c * QboundAbs b d <= `a * `b)%Q.
proof: Proof. intros. apply (Qle_trans _ _ _ (Qle_Qabs _)). rewrite Qabs_Qmult. rewrite QboundAbs_abs, QboundAbs_abs. apply (Qle_trans _ (`a * Qmin (Qabs d) (`b))). apply Qmult_le_compat_r. apply Qmin_lb_r. apply Qmin_glb. apply Qabs_nonneg. apply Qpos_nonneg. apply Qmult_le_l. apply Qpos_ispos. apply Qmin_lb_r. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names