proposition: Lemma RiemannInt_P20 : forall (f:R -> R) (a b:R) (h:a <= b) (pr:forall x:R, a <= x -> x <= b -> Riemann_integrable f a x) (pr0:Riemann_integrable f a b), RiemannInt pr0 = primitive h pr b - primitive h pr a.
proof: Proof. intros; replace (primitive h pr a) with 0. { replace (RiemannInt pr0) with (primitive h pr b). { ring. } unfold primitive; destruct (Rle_dec a b) as [Hle|[]]; destruct (Rle_dec b b) as [Hle'|Hnle']; [ apply RiemannInt_P5 | destruct Hnle'; right; reflexivity | assumption | assumption]. } symmetry ; unfold primitive; destruct (Rle_dec a a) as [Hle|[]]; destruct (Rle_dec a b) as [Hle'|Hnle']; [ apply RiemannInt_P9 | elim Hnle'; assumption | right; reflexivity | right; reflexivity ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra