proposition: Lemma derivable_pt_lim_comp : forall f1 f2 (x l1 l2:C), derivable_pt_lim f1 x l1 -> derivable_pt_lim f2 (f1 x) l2 -> derivable_pt_lim (comp f2 f1) x (l2 * l1).
proof: Proof. intros; assert (H1 := derivable_pt_lim_D_in f1 (fun y:C => l1) x). elim H1; intros. assert (H4 := H3 H). assert (H5 := derivable_pt_lim_D_in f2 (fun y:C => l2) (f1 x)). elim H5; intros. assert (H8 := H7 H0). clear H1 H2 H3 H5 H6 H7. assert (H1 := derivable_pt_lim_D_in (comp f2 f1)%F (fun y:C => l2 * l1) x). elim H1; intros. clear H1 H3; apply H2. unfold comp in |- *; cut (D_in (fun x0:C => f2 (f1 x0)) (fun y:C => l2 * l1) (Dgf no_cond no_cond f1) x -> D_in (fun x0:C => f2 (f1 x0)) (fun y:C => l2 * l1) no_cond x). intro; apply H1. rewrite Cmult_comm; apply (Dcomp no_cond no_cond (fun y:C => l1) (fun y:C => l2) f1 f2 x); assumption. unfold Dgf, D_in, no_cond in |- *; unfold limit1_in in |- *; unfold limit_in in |- *; unfold dist in |- *; simpl in |- *; unfold R_dist in |- *; intros. elim (H1 eps H3); intros. exists x0; intros; split. elim H5; intros; assumption. intros; elim H5; intros; apply H9; split. unfold D_x in |- *; split. split; trivial. elim H6; intros; unfold D_x in H10; elim H10; intros; assumption. elim H6; intros; assumption. Qed.
imports: MyRIneq Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_usual Ranalysis_facts Ranalysis_MVT Canalysis_diff Cprop_base Cnorm Ctacfield Cmet Canalysis_def Cderiv