proposition: Lemma continuity_div : forall f1 f2, continuity f1 -> continuity f2 -> (forall x, f2 x <> 0) -> continuity (f1 / f2).
proof: Proof. unfold continuity ; intros f1 f2 Hf1 Hf2 f2_neq x ; apply continuity_pt_div ; intuition. eapply f2_neq ; eassumption. Qed.
imports: Cfunctions Cprop_base Cbase Canalysis_def