proposition: Lemma continuity_inv : forall f, continuity f -> (forall x, f x <> 0) -> continuity (/ f).
proof: Proof. unfold continuity ; intros f Hf f_neq x ; apply continuity_pt_inv ; intuition. eapply f_neq ; eassumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def