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