proposition: Lemma LnegPartStable : forall {Elem : FunctionRieszSpace} (f : PartialFunction (X Elem)) (fL : L Elem f), L Elem (XnegPart f).
proof: Proof. intros. unfold XnegPart. apply LscaleStable. apply LminusStable. apply LabsStable. assumption. assumption. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions