proposition: Lemma continuity_implies_RiemannInt1 : forall (f:R -> R) (a b:R), (forall x:R, (a <= x <= b \/ b <= x <= a) -> continuity_pt f x) -> Riemann_integrable f a b.
proof: Proof. intros. destruct (Rle_dec a b). apply continuity_implies_RiemannInt; intuition. assert (b <= a) ; intuition. apply RiemannInt_P1. apply continuity_implies_RiemannInt; intuition. Qed.
imports: Reals integrales RiemannInt