proposition: Lemma Lim_inv (f : R -> R) (x : Rbar) : ex_lim f x -> Lim f x <> 0 -> Lim (fun y => / f y) x = Rbar_inv (Lim f x).
proof: Proof. move => /Lim_correct Hf Hlf. apply is_lim_unique. by apply is_lim_inv. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq