proposition: Lemma CR_b_upperBound_2 : forall x y : CR, (x * y <= 'proj1_sig ((CR_b (1#1) x) * CR_b (1#1) y)%Qpos)%CR.
proof: Proof. intros. rewrite <- (CRboundAbs_Eq (CR_b (1#1) x) (CR_b_lowerBound (1#1) x) (CR_b_upperBound (1#1) x)) at 1. unfold CRmult, ucFun2. intros e. simpl. unfold Cap_raw; simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. unfold Qminus. rewrite <- Qle_minus_iff. apply (QboundAbs_upperBound_2 (CR_b (1#1) x) (CR_b (1#1) y)). 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