proposition: Lemma Rint_Chasles : forall f a b c x y, Rint f a b x -> Rint f b c y -> Rint f a c (x+y).
proof: Proof. intros f a b c x y [prab Hab] [prbc Hbc]. pose proof (RiemannInt_P24 prab prbc) as prac. exists prac. rewrite <- Hab, <- Hbc. symmetry. apply RiemannInt_P26. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions