proposition: Lemma StepFun_P28 : forall (a b l:R) (f g:StepFun a b), IsStepFun (fun x:R => f x + l * g x) a b.
proof: Proof. intros a b l f g; unfold IsStepFun; assert (H := pre f); assert (H0 := pre g); unfold IsStepFun in H, H0; elim H; elim H0; intros; apply existT with (cons_ORlist x0 x); apply StepFun_P27; assumption. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra