proposition: Lemma continuity_div : forall f1 f2, continuity f1 -> continuity f2 -> (forall x:R, f2 x <> 0) -> continuity (f1 / f2).
proof: Proof. unfold continuity; intros; apply (continuity_pt_div f1 f2 x (H x) (H0 x) (H1 x)). Qed.
imports: Rbase Rfunctions Rlimit Rderiv