proposition: Lemma Rint_continuity : forall f a b, a <= b -> (forall x, a <= x <= b -> continuity_pt f x) -> {x : R & (Rint f a b x)}.
proof: Proof. intros f a b Hab f_cont. exists(RiemannInt (continuity_implies_RiemannInt Hab f_cont)). apply Rint_RiemannInt_link. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions