proposition: Lemma inv_sn_cv_0 : Rseq_cv inv_sn 0.
proof: Proof. intros e epos. assert (upepos : (0 < up (/ e))%Z). apply lt_IZR. eapply Rlt_trans. 2:apply (archimed (/e)). auto with *. assert (upenneg : (0 <= up (/ e))%Z) by auto with *. destruct (IZN _ upenneg) as (N, HN). exists N. intros n Hn. unfold R_dist, inv_sn. rewrite Rminus_0_r. rewrite Rabs_Rinv_pos; [ | INR_solve ]. rewrite <- (Rinv_involutive e); auto with *. apply Rinv_lt_contravar. apply Rmult_lt_0_compat; auto with *. eapply Rle_lt_trans with (INR n); [ | INR_solve ]. eapply Rle_trans with (IZR (up (/ e))). left. apply (archimed (/ e)). rewrite HN. rewrite <- INR_IZR_INZ. INR_solve. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra