proposition: Lemma ex_lim_seq_inv (u : nat -> R) : ex_lim_seq u -> Lim_seq u <> 0 -> ex_lim_seq (fun n => / u n).
proof: Proof. intros. apply Lim_seq_correct in H. exists (Rbar_inv (Lim_seq u)). by apply is_lim_seq_inv. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy