proposition: Lemma derivable_pt_lim_in_mult: forall (D : R -> Prop) f g x l1 l2, D x -> derivable_pt_lim_in D f x l1 -> derivable_pt_lim_in D g x l2 -> derivable_pt_lim_in D (f * g)%F x (l1 * g x + f x * l2).
proof: Proof. intros D f g x l1 l2 Dx Hf Hg ; eapply limit1_in_ext. intros y [Dy Hneq] ; symmetry ; apply growth_rate_mult_decomp, Hneq. apply limit_plus ; apply limit_mul ; [apply Hf | | | apply Hg]. apply limit_free. apply limit1_imp with D. intros y [y_in y_neq] ; exact y_in. apply derivable_pt_in_continuity_pt_in ; [eexists |] ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics