proposition: Lemma continuity_implies_ex_Rint: forall f a b, (forall x, continuity_pt f x) -> ex_RInt f a b.
proof: Proof. intros f a b H. case (Rle_or_lt a b); intros H1. apply ex_RInt_Reals_1. apply continuity_implies_RiemannInt. exact H1. intros x _; apply H. apply ex_RInt_swap. apply ex_RInt_Reals_1. apply continuity_implies_RiemannInt. left; exact H1. intros x _; apply H. Qed.
imports: Coq(Reals ssreflect) Coquelicot(Rcomplements Derive RInt Hierarchy Derive_2d AutoDerive)