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