proposition: Lemma RiemannInt_P24 : forall (f:R -> R) (a b c:R), Riemann_integrable f a b -> Riemann_integrable f b c -> Riemann_integrable f a c.
proof: Proof. intros; case (Rle_dec a b); case (Rle_dec b c); intros. - apply RiemannInt_P21 with b; assumption. - case (Rle_dec a c); intro. + apply RiemannInt_P22 with b; try assumption. split; [ assumption | auto with real ]. + apply RiemannInt_P1; apply RiemannInt_P22 with b. * apply RiemannInt_P1; assumption. * split; auto with real. - case (Rle_dec a c); intro. + apply RiemannInt_P23 with b; try assumption. split; auto with real. + apply RiemannInt_P1; apply RiemannInt_P23 with b. * apply RiemannInt_P1; assumption. * split; [ assumption | auto with real ]. - apply RiemannInt_P1; apply RiemannInt_P21 with b; auto with real || apply RiemannInt_P1; assumption. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra