proposition: Lemma is_lim_RInv_p_infty: is_lim [eta Rinv] p_infty 0.
proof: Proof. suff -> : 0 = Rbar_inv p_infty => // . apply: (is_lim_inv (fun x => x) p_infty p_infty) => // . Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval