proposition: Lemma applyXnegPart : forall {R : ConstructiveReals} {X : Set} (f : @PartialFunction R X) (x : X) (xD : Domain f x), partialApply (XnegPart f) x (pair xD xD) == CRmax 0 (- partialApply f x xD).
proof: Proof. intros. rewrite XnegPartAbsMax. unfold XnegPart. rewrite applyXscale, CRmult_comm. apply CRmult_morph. 2: reflexivity. rewrite (applyXminus (Xabs f) f). apply CRplus_morph. rewrite applyXabs. apply CRabs_morph. apply DomainProp. reflexivity. Qed.
imports: List QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete