proposition: Lemma splitIntegralPosNeg : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f), I IS f fL == (I IS (XposPart f) (LposPartStable f fL)) - (I IS (XnegPart f) (LnegPartStable f fL)).
proof: Proof. intros. rewrite <- (CRmult_1_l (I IS (XnegPart f) (LnegPartStable f fL))). unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- Ihomogeneous. rewrite <- Iadditive. apply IExtensional. intros. destruct y. rewrite (applyXplus (XposPart f) (Xscale (- (1)) (XnegPart f))). rewrite applyXscale. unfold XposPart, XnegPart. do 2 rewrite applyXscale. destruct d. rewrite (applyXplus f (Xabs f) x). destruct d0. rewrite (applyXminus (Xabs f) f). do 2 rewrite applyXabs. rewrite (DomainProp f x d1 d), (DomainProp f x d2 d), (DomainProp f x d0 d), (DomainProp f x xF d). generalize (partialApply f x d). intros. rewrite <- CRopp_mult_distr_l, CRmult_1_l. rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. setoid_replace (c + CRabs _ c + - (CRabs _ c + - c)) with (CR_of_Q _ 2 * c). rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. rewrite CRmult_1_l. reflexivity. reflexivity. rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_r. rewrite CRmult_1_l, CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr, <- CRplus_assoc, CRplus_opp_r. rewrite CRplus_0_l, CRopp_involutive. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase