proposition: Lemma phi_sequence_prop : forall (un:nat -> posreal) (f:R -> R) (a b:R) (pr:Riemann_integrable f a b) (N:nat), { psi:StepFun a b | (forall t:R, Rmin a b <= t <= Rmax a b -> Rabs (f t - phi_sequence un pr N t) <= psi t) /\ Rabs (RiemannInt_SF psi) < un N }.
proof: Proof. intros; apply (projT2 (pr (un N))). Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra