proposition: Lemma Riemann_integrable_ext : forall f g a b, (forall x, Rmin a b <= x <= Rmax a b -> f x = g x) -> Riemann_integrable f a b -> Riemann_integrable g a b.
proof: Proof. intros f g a b fg rif eps; destruct (rif eps) as [phi [psi [P1 P2]]]. exists phi; exists psi;split;[ | assumption ]. intros t intt; rewrite <- fg;[ | assumption]. apply P1; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra