proposition: Lemma StepFun_P37 : forall (a b:R) (f g:StepFun a b), a <= b -> (forall x:R, a < x < b -> f x <= g x) -> RiemannInt_SF f <= RiemannInt_SF g.
proof: Proof. intros; eapply StepFun_P36; try assumption. - eapply StepFun_P25; apply StepFun_P29. - eapply StepFun_P23; apply StepFun_P29. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra