fact: Definition primitive (f:R -> R) (a b:R) (h:a <= b) (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x) (x:R) : R := match Rle_dec a x with | left r => match Rle_dec x b with | left r0 => RiemannInt (pr x r r0) | right _ => f b * (x - b) + RiemannInt (pr b h (Rle_refl b)) end | right _ => f a * (x - a) end.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra