proposition: Lemma continuity_pt_inv : forall f z, continuity_pt f z -> f z <> 0 -> continuity_pt (/ f) z.
proof: Proof. intros f z f_cont Fz_neq ; replace (/ f)%F with (fun z => / f z). intros eps eps_pos ; apply limit_inv ; assumption. unfold inv_fct ; reflexivity. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def