proposition: Lemma IntegralScale : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fInt : IntegrableFunction f) (a : CRcarrier (RealT (ElemFunc IS))), Integral (IntegrableScale f a fInt) == (Integral fInt) * a.
proof: Proof. intros. unfold IntegrableScale, IntegralRepresentationScale, Integral. do 2 rewrite IntegralRepresentationWeaveSum. do 2 rewrite IntegralHomogeneousHalf. unfold Integral. rewrite <- CRopp_mult_distr_r, CRmult_1_r, CRplus_opp_r. rewrite CRplus_0_r. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase