proposition: Lemma C_mult : forall n f g, C n f -> C n g -> C n (f * g)%F.
proof: Proof. intro n ; induction n ; intros f g Cnf Cng ; inversion Cnf ; inversion Cng ; subst. constructor ; reg. assert (pr1 : derivable (f * g)%F) by reg ; apply C_S with pr1 ; apply C_ext with (fun x => (derive f pr) x * g x + f x * (derive g pr0) x)%R. intro x ; symmetry ; unfold derive ; rewrite derive_pt_eq ; eapply derive_pt_eq_1 ; apply derive_pt_mult. apply C_plus ; apply IHn ; [| apply C_pred | apply C_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