proposition: Lemma FTC_P1 : forall (f:R -> R) (a b:R), a <= b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> forall x:R, a <= x -> x <= b -> Riemann_integrable f a x.
proof: Proof. intros; apply continuity_implies_RiemannInt; [ assumption | intros; apply H0; elim H3; intros; split; assumption || apply Rle_trans with x; assumption ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra