proposition: Lemma Rint_opp1 : forall f a b x, Rint f a b x -> Rint (- f)%F a b (- x).
proof: Proof. intros f a b x; intros [prf Hf]; unfold opp_fct. apply Rint_eq_compat with (fun u => fct_cte 0 u + (-1) * f u). unfold fct_cte; intros; ring. replace (- x) with (0 + (-1)* x) by ring. pose proof Rint_constant 0 a b as [prg Hg]. pose proof RiemannInt_P10 (-1) prg prf as prfg. exists prfg. rewrite RiemannInt_P13 with _ _ _ _ _ prg prf prfg. rewrite Hf, Hg; ring. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions