proposition: Lemma derivable_minus : forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2).
proof: Proof. unfold derivable; intros f1 f2 X X0 x. apply (derivable_pt_minus _ _ x (X _) (X0 _)). Qed.
imports: Rbase Rfunctions Rlimit Rderiv