proposition: Lemma RiemannInt_P19 : forall (f g:R -> R) (a b:R) (pr1:Riemann_integrable f a b) (pr2:Riemann_integrable g a b), a <= b -> (forall x:R, a < x < b -> f x <= g x) -> RiemannInt pr1 <= RiemannInt pr2.
proof: Proof. intro f; intros; apply Rplus_le_reg_l with (- RiemannInt pr1); rewrite Rplus_opp_l; rewrite Rplus_comm; apply Rle_trans with (Rabs (RiemannInt (RiemannInt_P10 (-1) pr2 pr1))). { apply Rabs_pos. } replace (RiemannInt pr2 + - RiemannInt pr1) with (RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) pr2 pr1))). { apply (RiemannInt_P17 (RiemannInt_P10 (-1) pr2 pr1) (RiemannInt_P16 (RiemannInt_P10 (-1) pr2 pr1))); assumption. } replace (RiemannInt pr2 + - RiemannInt pr1) with (RiemannInt (RiemannInt_P10 (-1) pr2 pr1)). { apply RiemannInt_P18; try assumption. intros; apply Rabs_right. apply Rle_ge; apply Rplus_le_reg_l with (f x); rewrite Rplus_0_r; replace (f x + (g x + -1 * f x)) with (g x); [ apply H0; assumption | ring ]. } rewrite (RiemannInt_P12 pr2 pr1 (RiemannInt_P10 (-1) pr2 pr1)); [ ring | assumption ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra