fact: Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) : list R := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) end.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra