proposition: Lemma derivable_pt_lim_comp : forall f1 f2 (x l1 l2:R), derivable_pt_lim f1 x l1 -> derivable_pt_lim f2 (f1 x) l2 -> derivable_pt_lim (f2 o f1) x (l2 * l1).
proof: Proof. intros; assert (H1 := derivable_pt_lim_D_in f1 (fun y:R => l1) x). elim H1; intros. assert (H4 := H3 H). assert (H5 := derivable_pt_lim_D_in f2 (fun y:R => l2) (f1 x)). elim H5; intros. assert (H8 := H7 H0). clear H1 H2 H3 H5 H6 H7. assert (H1 := derivable_pt_lim_D_in (f2 o f1)%F (fun y:R => l2 * l1) x). elim H1; intros. clear H1 H3; apply H2. unfold comp; cut (D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1) (Dgf no_cond no_cond f1) x -> D_in (fun x0:R => f2 (f1 x0)) (fun y:R => l2 * l1) no_cond x). - intro; apply H1. rewrite Rmult_comm; apply (Dcomp no_cond no_cond (fun y:R => l1) (fun y:R => l2) f1 f2 x); assumption. - unfold Dgf, D_in, no_cond; unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. elim (H1 eps H3); intros. exists x0; intros; split. + elim H5; intros; assumption. + intros; elim H5; intros; apply H9; split. * unfold D_x; split. -- split; trivial. -- elim H6; intros; unfold D_x in H10; elim H10; intros; assumption. * elim H6; intros; assumption. Qed.
imports: Rbase Rfunctions Rlimit Rderiv