proposition: Lemma D_Rball_mult : forall c r n f g, D_Rball c r n f -> D_Rball c r n g -> D_Rball c r n (f * g)%F.
proof: Proof. intros c r n ; induction n ; intros f g Dnf Dng ; inversion Dnf ; inversion Dng ; subst. constructor. assert (pr1 : derivable_in (Rball c r) (f * g)%F) by (apply derivable_in_mult ; assumption). apply Db_S with pr1 ; apply D_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 D_Rball_plus ; apply IHn ; [| apply D_Rball_pred | apply D_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