proposition: Lemma continuity_pt_div : forall f1 f2 z, continuity_pt f1 z -> continuity_pt f2 z -> f2 z <> 0 -> continuity_pt (f1 / f2) z.
proof: Proof. intros ; rewrite div_eq_inv ; apply continuity_pt_mult ; [| apply continuity_pt_inv] ; assumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def