proposition: Lemma LminIntStable : forall {E : FunctionRieszSpace} (n : nat) (f : PartialFunction (X E)), L E f -> L E (XminConst f (INR n)).
proof: Proof. intros E n f H. destruct n. - apply (Lext _ (Xscale (-(1)) (XnegPart f))). 2: apply LscaleStable, LnegPartStable, H. split. split. + intros x xd. destruct f; apply xd. + intros x xd. destruct f; split; apply xd. + intros. rewrite applyXscale, applyXminConst. simpl in xD, xG. rewrite (DomainProp (XnegPart f) x _ (xG, xG)). rewrite (applyXnegPartMin f x xG), <- CRopp_mult_distr_l. rewrite CRmult_1_l, CRopp_involutive, CRmin_sym. apply CRmin_morph. reflexivity. reflexivity. - apply LminConstStable. apply CR_of_Q_lt. reflexivity. exact H. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions