proposition: Lemma RiemannInt_P320 : forall (f:R -> R) (H : derivable f) (cont1 : continuity (derive f H))(a b:R), Riemann_integrable (derive f H) a b.
proof: Proof. intro f; intros; case (Rle_dec a b); intro; [ apply continuity_implies_RiemannInt; try assumption; intros; apply (cont1) | assert (H1 : b <= a); [ auto with real | apply RiemannInt_P1; apply continuity_implies_RiemannInt; try assumption; intros; apply (cont1) ] ]. Qed.
imports: Reals integrales RiemannInt