fact: Fixpoint Int_SF (l k:list R) : R := match l with | nil => 0 | cons a l' => match k with | nil => 0 | cons x nil => 0 | cons x (cons y k') => a * (y - x) + Int_SF l' (cons y k') end end.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra