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