proposition: Lemma RiemannInt_exists : forall (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) (un:nat -> posreal), Un_cv un 0 -> { l:R | Un_cv (fun N:nat => RiemannInt_SF (phi_sequence un pr N)) l }.
proof: Proof. intros f; intros; apply RiemannInt_P3 with f un (fun n:nat => proj1_sig (phi_sequence_prop un pr n)); [ apply H | intro; apply (proj2_sig (phi_sequence_prop un pr n)) ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra