proposition: Lemma Rint_subinterval : forall f a b c x, (a <= b <= c) -> Rint f a c x -> {y : R & Rint f a b y & Rint f b c (x-y)}.
proof: Proof. intros f a b c x Hb [prac Hf]. pose proof RiemannInt_P22 prac Hb as prab. exists (RiemannInt prab). apply Rint_RiemannInt_link. pose proof RiemannInt_P23 prac Hb as prbc. exists prbc. rewrite <- Hf. rewrite <- RiemannInt_P26 with _ _ _ _ prab prbc prac. ring. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions