proposition: Lemma IabsHomogeneous : forall {IS : IntegrationSpace} (a : CRcarrier (RealT (ElemFunc IS))) (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f), Iabs (Xscale a f) (LscaleStable (ElemFunc IS) a f fL) == (CRabs _ a) * Iabs f fL.
proof: Proof. intros. unfold Iabs. rewrite <- Ihomogeneous. apply IExtensional. intros. destruct f; simpl. rewrite CRabs_mult. apply CRmult_morph. reflexivity. rewrite (DomainProp x xF y). reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions