proposition: Lemma is_lim_inv (f : R -> R) (x l : Rbar) : is_lim f x l -> l <> 0 -> is_lim (fun y => / f y) x (Rbar_inv l).
proof: Proof. intros Hf Hl. apply filterlim_comp with (1 := Hf). now apply filterlim_Rbar_inv. Qed.
imports: Coq(Reals ssreflect) Rcomplements Rbar Hierarchy Compactness Lim_seq