proposition: Lemma An_squared_Bn_cv : Rseq_cv (An * An - Bn) 0.
proof: Proof. intros e epos. destruct (abound_cv e epos) as [N H]. exists (S N); intros n nN. unfold R_dist; rewrite Rminus_0_r. unfold Rseq_minus, Rseq_mult, Rseq_abs. eapply Rle_lt_trans. apply An_squared_Bn_maj. lia. assert (nN' : (n >= N)%nat) by lia. pose proof (H n nN') as T. unfold R_dist in T; rewrite Rminus_0_r in T. eapply Rle_lt_trans. 2: apply T. apply RRle_abs. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith