proposition: Lemma continuity_inv : forall f, continuity f -> (forall x:R, f x <> 0) -> continuity (/ f).
proof: Proof. unfold continuity; intros; apply (continuity_pt_inv f x (H x) (H0 x)). Qed.
imports: Rbase Rfunctions Rlimit Rderiv