proposition: Lemma derivable_pt_comp : forall f1 f2 (x:R), derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x.
proof: Proof. unfold derivable_pt; intros f1 f2 x X X0. elim X; intros. elim X0; intros. exists (x1 * x0). apply derivable_pt_lim_comp; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv