proposition: Lemma derivable_pt_lim_Rball_comp: forall cf rf cg rg f g x l1 l2, Rball cf rf x -> Rball cg rg (f x) -> derivable_pt_lim_in (Rball cf rf) f x l1 -> derivable_pt_lim_in (Rball cg rg) g (f x) l2 -> derivable_pt_lim_in (Rball cf rf) (comp g f) x (l1 * l2).
proof: Proof. intros cf rf cg rg f g x l1 l2 x_in fx_in Hf Hg ; rewrite Rmult_comm. apply derivable_pt_lim_derivable_pt_lim_in, derivable_pt_lim_comp ; eapply derivable_pt_lim_Rball_pt_lim ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics