proposition: Lemma inverse_cv_0 : Rseq_cv (fun i => / INR (S i)) 0.
proof: Proof. apply Rseq_cv_pos_infty_inv_compat. assert (H01 : (1 > 0)%nat) by lia. pose proof (Rseq_poly_cv 1 H01). unfold Rseq_poly in H; simpl in H. eapply Rseq_cv_pos_infty_eq_compat in H; [ | intro; apply Rmult_1_r]. intro M. destruct (H M) as [N Hcv]. exists N. intros. eapply Rlt_le_trans. apply Hcv. apply H0. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith