proposition: Lemma QboundAbs_lowerBound_2 : forall (a b : Qpos) (c d : Q), (- (`a * `b) <= QboundAbs a c * QboundAbs b d)%Q.
proof: Proof. intros. apply (Qle_trans _ (-Qabs (QboundAbs a c * QboundAbs b d))). apply Qopp_le_compat. 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. rewrite <- (Qopp_involutive (QboundAbs a c * QboundAbs b d)) at 2. apply Qopp_le_compat. rewrite <- Qabs_opp. apply Qle_Qabs. 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