proposition: Lemma RiemannInt_opp : forall (f : R -> R) (a b : R) (pr_f : Riemann_integrable f a b) (pr : Riemann_integrable (fun x => - f x) a b), RiemannInt pr = - RiemannInt pr_f.
proof: Proof. intros. rewrite <- (Rmult_1_l (RiemannInt pr_f)). rewrite <- Ropp_mult_distr_l_reverse. rewrite -(Rplus_0_l (-1 * RiemannInt pr_f)). assert (0 = RiemannInt (Riemann_integrable_const 0 a b)). rewrite RiemannInt_const. ring. rewrite H ; clear H. rewrite <- (RiemannInt_P13 (Riemann_integrable_const 0 _ _) pr_f (RiemannInt_P10 (-1) (Riemann_integrable_const 0 a b) pr_f)). apply RiemannInt_ext. intros ; ring. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)