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