fact: Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := match Rle_dec a b with | left _ => Int_SF (subdivision_val f) (subdivision f) | right _ => - Int_SF (subdivision_val f) (subdivision f) end.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra