proposition: Lemma derivable_pt_Rball_comp: forall cf rf cg rg f g x, Rball cf rf x -> Rball cg rg (f x) -> derivable_pt_in (Rball cf rf) f x -> derivable_pt_in (Rball cg rg) g (f x) -> derivable_pt_in (Rball cf rf) (comp g f) x.
proof: Proof. intros cf rf cg rg f g x x_in y_in [] [] ; eexists ; eapply derivable_pt_lim_Rball_comp ; eassumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity MyRIneq MyR_dist Lra Tactics