proposition: Lemma LminConstStable : forall {E : FunctionRieszSpace} (a : CRcarrier (RealT E)) (f : PartialFunction (X E)), 0 < a -> L E f -> L E (XminConst f a).
proof: Proof. intros. apply (Lext _ _ _ (XminMultPosDistribOne f a H)). apply LscaleStable. apply LminOneStable. apply LscaleStable. assumption. Defined.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions