proposition: Lemma continuity_RiemannInt_1 : 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; case (total_order_T a b); intro. elim s ; intro. apply RiemannInt_P6. assumption. intros. apply H. intuition. subst; apply RiemannInt_P7. apply Riemann_integrable_opp_bound. apply RiemannInt_P6. intuition. intros. apply H. intuition. Qed.
imports: PeanoNat Reals Lra RiemannInt Rfunction_classes_def Rextensionality