proposition: Lemma RiemannInt_P5 : forall (f:R -> R) (a b:R) (pr1 pr2:Riemann_integrable f a b), RiemannInt pr1 = RiemannInt pr2.
proof: Proof. intros; unfold RiemannInt; case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x,HUn); case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x0,HUn0); eapply UL_sequence; [ apply HUn | apply RiemannInt_P4 with pr2 RinvN; apply RinvN_cv || assumption ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra