proposition: Lemma C_Rball_mult : forall c r n f g, C_Rball c r n f -> C_Rball c r n g -> C_Rball c r n (f * g)%F.
proof: Proof. intros c r n ; induction n ; intros f g Cnf Cng ; inversion Cnf ; inversion Cng ; subst. constructor ; intros x x_in ; apply limit_mul ; eapply_assumption ; assumption. assert (pr1 : derivable_in (Rball c r) (f * g)%F) by (apply derivable_in_mult ; assumption). apply Cb_S with pr1 ; apply C_Rball_ext with (fun x => (derive_Rball c r f pr) x * g x + f x * (derive_Rball c r g pr0) x)%R. apply Req_Rball_eq ; intro ; symmetry ; apply derive_Rball_mult. apply C_Rball_plus ; apply IHn ; [| apply C_Rball_pred | apply C_Rball_pred |] ; 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