proposition: Lemma Riemann_integrable_Ropp : forall f a b, Riemann_integrable f a b -> Riemann_integrable (fun x => - f x) a b.
proof: Proof. intros ff a b h. apply Riemann_integrable_ext with (f := fun x => (-1) * ff x). { intros; ring. } apply Riemann_integrable_scal; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra