proposition: Lemma CRmult_bounded_mult : forall (c:Qpos) (x y:CR), (' (-proj1_sig c)%Q <= y -> y <= ' proj1_sig c -> CRmult_bounded c x y == x*y)%CR.
proof: Proof. intros c x y Hc1 Hc2. unfold CRmult. set (d:=(CR_b (1 # 1) y)). destruct (Qle_total (proj1_sig c) (proj1_sig d)). apply CRmult_bounded_weaken; assumption. symmetry. apply CRmult_bounded_weaken; try assumption. apply CR_b_lowerBound. apply CR_b_upperBound. 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