proposition: Lemma is_lim_Rinv_0_right (f : R -> R) (x : Rbar) : is_lim f x 0 -> Rbar_locally' x (fun x => 0 < f x) -> is_lim (fun x => / (f x)) x p_infty.
proof: Proof. intros. eapply filterlim_comp, filterlim_Rinv_0_right. intros P HP. apply H in HP. generalize (filter_and _ _ H0 HP). rewrite /filtermap ; apply filter_imp => y Hy. by apply Hy, Hy. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis