proposition: Lemma C_Rball_ext: forall c r n f g, Rball_eq c r f g -> C_Rball c r n f -> C_Rball c r n g.
proof: Proof. intros c r n ; induction n ; intros f g Heq Hf ; inversion_clear Hf. constructor ; eapply continuity_in_ext_strong ; eassumption. assert (g_deriv: derivable_Rball c r g) by (eapply derivable_in_ext_strong ; eassumption). apply (Cb_S _ _ _ _ g_deriv), IHn with (derive_Rball _ _ _ pr). intros x x_in ; eapply derive_Rball_ext_strong ; eassumption. assumption. Qed.
imports: Rbase Ranalysis Lia Lra Rfunctions Rfunction_facts Rextensionality Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rfunction_classes_def MyR_dist Reals.Tactics