proposition: Lemma continuity_pt_div : forall f1 f2 (x0:R), continuity_pt f1 x0 -> continuity_pt f2 x0 -> f2 x0 <> 0 -> continuity_pt (f1 / f2) x0.
proof: Proof. intros; rewrite (div_eq_inv f1 f2); apply continuity_pt_mult; [ assumption | apply continuity_pt_inv; assumption ]. Qed.
imports: Rbase Rfunctions Rlimit Rderiv