proposition: Lemma CRmult_scale : forall (a:Q) (y:CR), ((' a)*y==scale a y)%CR.
proof: Proof. intros a y. unfold CRmult. unfold CRmult_bounded. unfold ucFun2. unfold Cmap2. unfold inject_Q_CR. change (msp_eq (Cap_fun QPrelengthSpace (Cmap_fun QPrelengthSpace (Qmult_uc (CR_b (1 ↾ eq_refl) y)) (Cunit_fun Q_as_MetricSpace a)) y) (Cmap_fun QPrelengthSpace (Qscale_uc a) y)). rewrite -> Cap_fun_correct. repeat rewrite -> Cmap_fun_correct. rewrite -> MonadLaw3. rewrite -> StrongMonadLaw1. change (msp_eq (Cmap_slow_fun (Qscale_uc a ∘ QboundAbs (CR_b (1 ↾ eq_refl) y)) y) (Cmap_slow_fun (Qscale_uc a) y)). transitivity (uc_compose (Cmap QPrelengthSpace (Qscale_uc a)) (Cmap QPrelengthSpace (QboundAbs (CR_b (1#1) y))) y). simpl ((Cmap QPrelengthSpace (Qscale_uc a) ∘ Cmap QPrelengthSpace (QboundAbs (CR_b (1 ↾ eq_refl) y))) y). repeat rewrite -> Cmap_fun_correct. apply MonadLaw2. simpl ((Cmap QPrelengthSpace (Qscale_uc a) ∘ Cmap QPrelengthSpace (QboundAbs (CR_b (1 ↾ eq_refl) y))) y). repeat rewrite -> Cmap_fun_correct. change (Cmap_slow (Qscale_uc a) (Cmap_slow_fun (QboundAbs (CR_b (1 # 1) y)) y) == Cmap_slow (Qscale_uc a) y)%CR. apply uc_wd. rewrite <- (Cmap_fun_correct (Y:=Q_as_MetricSpace) QPrelengthSpace). apply CRboundAbs_Eq. 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