proposition: Lemma continuity_pt_scal : forall f a z, continuity_pt f z -> continuity_pt (mult_real_fct a f) z.
proof: Proof. intros; apply (limit_mul (fun x:C => a) f (D_x no_cond z) a (f z) z). intros ; exists 1%R ; split. apply Rlt_0_1. intros; rewrite C_dist_eq ; intuition. assumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def