proposition: Lemma RiemannInt_P310 : forall (f:R -> R) (H : derivable f) (cont1 : continuity (derive f H)) (a b:R), a <= b -> antiderivative (derive f H) f a b.
proof: Proof. intro f; intros; unfold antiderivative in |- *; split; try assumption; intros; split with (H x); reflexivity. Qed.
imports: Reals integrales RiemannInt