proposition: Lemma QboundAbs_mult : forall (a b : Q) (c : Qpos), -(`c*`c) <= QboundAbs c a * QboundAbs c b.
proof: Proof. intros. destruct (Qlt_le_dec 0 a). - assert (-`c <= QboundAbs c b) by apply Qmax_ub_l. apply (Qmult_le_compat_r _ _ (QboundAbs c a)) in H. rewrite (Qmult_comm (QboundAbs c b)) in H. refine (Qle_trans _ _ _ _ H). setoid_replace (- ` c * QboundAbs c a)%Q with (-(` c * QboundAbs c a))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qopp_le_compat. apply Qmult_le_l. apply Qpos_ispos. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. apply (Qle_trans _ (Qmin (`c) a)). apply Qmin_glb. apply Qpos_nonneg. apply Qlt_le_weak, q. apply Qmax_ub_r. - rewrite <- (Qopp_involutive (QboundAbs c a * QboundAbs c b)). apply Qopp_le_compat. assert (QboundAbs c b <= `c)%Q. { apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } apply (Qmult_le_compat_r _ _ (-QboundAbs c a)) in H. rewrite Qmult_comm in H. setoid_replace (-(QboundAbs c a * QboundAbs c b))%Q with (- QboundAbs c a * QboundAbs c b)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ H). apply Qmult_le_l. apply Qpos_ispos. rewrite <- (Qopp_involutive (`c)). apply Qopp_le_compat. apply Qmax_ub_l. apply (Qopp_le_compat _ 0). apply Qmax_lub. apply (Qopp_le_compat 0), Qpos_nonneg. apply (Qle_trans _ a). apply Qmin_lb_r. exact q. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders