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