proposition: Lemma continuity_pt_mult : forall f1 f2 z, continuity_pt f1 z -> continuity_pt f2 z -> continuity_pt (f1 * f2) z.
proof: Proof. intros ; apply limit_mul; assumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def