proposition: Lemma C_Rball_scal : forall c r n f a, C_Rball c r n f -> C_Rball c r n (mult_real_fct a f).
proof: Proof. intros c r n ; induction n ; intros f a Cnf ; inversion_clear Cnf. constructor ; intros x x_in ; eapply limit_scal ; do 2 eapply_assumption. apply Cb_S with (derivable_in_scal _ _ _ pr) ; apply C_Rball_ext with (mult_real_fct a (derive_Rball c r f pr)). intros x x_in ; symmetry ; apply derive_Rball_scal. apply IHn ; 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