proposition: Lemma continuity_pt_inv : forall f (x0:R), continuity_pt f x0 -> f x0 <> 0 -> continuity_pt (/ f) x0.
proof: Proof. intros. replace (/ f)%F with (fun x:R => / f x). - unfold continuity_pt; unfold continue_in; intros; apply limit_inv; assumption. - unfold inv_fct; reflexivity. Qed.
imports: Rbase Rfunctions Rlimit Rderiv