proposition: Lemma RiemannInt_P26 : forall (f:R -> R) (a b c:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c), RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3.
proof: Proof. intros; destruct (Rle_dec a b) as [Hle|Hnle]; destruct (Rle_dec b c) as [Hle'|Hnle']. - apply RiemannInt_P25; assumption. - destruct (Rle_dec a c) as [Hle''|Hnle'']. { assert (H : c <= b). { auto with real. } rewrite <- (RiemannInt_P25 pr3 (RiemannInt_P1 pr2) pr1 Hle'' H); rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); ring. } assert (H : c <= a). { auto with real. } rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr3) pr1 (RiemannInt_P1 pr2) H Hle); rewrite (RiemannInt_P8 pr3 (RiemannInt_P1 pr3)); ring. - assert (H : b <= a). { auto with real. } destruct (Rle_dec a c) as [Hle''|Hnle'']. { rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr1) pr3 pr2 H Hle''); rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); ring. } assert (H0 : c <= a). { auto with real. } rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); rewrite <- (RiemannInt_P25 pr2 (RiemannInt_P1 pr3) (RiemannInt_P1 pr1) Hle' H0); rewrite (RiemannInt_P8 pr3 (RiemannInt_P1 pr3)); ring. - rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); rewrite (RiemannInt_P8 pr3 (RiemannInt_P1 pr3)); rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr2) (RiemannInt_P1 pr1) (RiemannInt_P1 pr3)) ; [ ring | auto with real | auto with real ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra