proposition: Lemma SplitPosNegParts : forall {X : Set} {R : ConstructiveReals} (f : @PartialFunction R X) (x : X) (xdf : Domain f x) (xdp : Domain (XposPart f) x) (xdn : Domain (XnegPart f) x), partialApply (XposPart f) x xdp - partialApply (XnegPart f) x xdn == partialApply f x xdf.
proof: Proof. intros. unfold XposPart, XnegPart, CRminus. do 2 rewrite applyXscale. destruct xdp. rewrite (applyXplus f (Xabs f)). destruct xdn. rewrite (applyXminus (Xabs f) f). rewrite CRplus_comm. unfold CRminus. rewrite (DomainProp f x _ xdf), (DomainProp (Xabs f) x _ xdf). rewrite CRopp_mult_distr_r, <- CRmult_plus_distr_l. rewrite (DomainProp f x d xdf), (DomainProp (Xabs f) x d0 xdf). setoid_replace (- (partialApply (Xabs f) x xdf + - partialApply f x xdf) + (partialApply f x xdf + partialApply (Xabs f) x xdf)) with (partialApply f x xdf + partialApply f x xdf). rewrite <- (CRmult_1_l (partialApply f x xdf)), <- CRmult_plus_distr_r. rewrite <- CRmult_assoc, CRmult_1_l, <- CR_of_Q_plus. rewrite <- CR_of_Q_mult. setoid_replace ((1 # 2) * (1+1))%Q with 1%Q. apply CRmult_1_l. reflexivity. rewrite CRplus_comm, CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRopp_plus_distr. rewrite CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete