proposition: Lemma derivable_pt_lim_mult : forall f1 f2 x l1 l2, derivable_pt_lim f1 x l1 -> derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 * f2) x (l1 * f2 x + f1 x * l2).
proof: Proof. intros. assert (H1 := derivable_pt_lim_D_in f1 (fun y => l1) x). elim H1; intros. assert (H4 := H3 H). assert (H5 := derivable_pt_lim_D_in f2 (fun y => l2) x). elim H5; intros. assert (H8 := H7 H0). clear H1 H2 H3 H5 H6 H7. assert (H1 := derivable_pt_lim_D_in (f1 * f2)%F (fun y => l1 * f2 x + f1 x * l2) x). elim H1; intros. clear H1 H3. apply H2. unfold mult_fct in |- *. apply (Dmult no_cond (fun y => l1) (fun y => l2) f1 f2 x); 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