proposition: Lemma RiemannInt_P9 : forall (f:R -> R) (a:R) (pr:Riemann_integrable f a a), RiemannInt pr = 0.
proof: Proof. intros; assert (H := RiemannInt_P8 pr pr); apply Rmult_eq_reg_l with 2; [ rewrite Rmult_0_r; rewrite <-Rplus_diag; pattern (RiemannInt pr) at 2; rewrite H; apply Rplus_opp_r | discrR ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra