proposition: Lemma An_squared_Bn_maj : forall N, (1 <= N)%nat -> Rabs (An N * An N - Bn N) <= abound N.
proof: Proof. intros N H. destruct N. inversion H. rewrite calc3. rewrite sum_bisum. eapply Rle_trans; [apply Rabs_triang | ]. unfold abound. assert (REWdiv : forall a b, pow1 a / b = pow1 a * / b) by reflexivity. replace (sum_f_R0 (fun n : nat => / INR (S N - S n + 1) * (/ INR (2 * n + 1) + / INR (2 * n + 3))) (pred (S N))) with (sum_f_R0 (fun n : nat => / INR (S N - S n + 1) * / INR (2 * n + 3)) (pred (S N)) + sum_f_R0 (fun n : nat => / INR (S N - S n + 1) * / INR (2 * n + 1)) (pred (S N))) by ( rewrite <- plus_sum; simpl pred; apply Rseq_sum_ext; intro n; field; INR_solve ). rewrite decomp_sum by lia; simpl pred; simpl (Z_of_nat 0); rewrite cn_zero_zero; rewrite Rmult_0_r; rewrite Rplus_0_l. apply Rplus_le_compat. eapply Rle_trans; [apply Rsum_abs | ]. replace (pred (S (S N))) with (S N) by trivial. apply sum_Rle; intros n nSN. rewrite REWdiv. repeat rewrite Rabs_mult. rewrite pow1_Rabs; rewrite Rmult_1_l. rewrite Rmult_comm. apply Rmult_le_compat; try apply Rabs_pos. apply (cn_maj (S n) (S N)); lia. unfold d', d; rewrite <- INR_IZR_INZ. rewrite Rabs_pos_eq; try apply Rle_Rinv; try (apply Rlt_le; apply Rinv_0_lt_compat); INR_solve. eapply Rle_trans; [apply Rsum_abs | ]. replace (pred (S (S N))) with (S N) by trivial. apply sum_Rle; intros n nSN. rewrite REWdiv. repeat rewrite Rabs_mult. rewrite pow1_Rabs; rewrite Rmult_1_l. rewrite Rmult_comm. apply Rmult_le_compat; try apply Rabs_pos. eapply Rle_trans. rewrite cn_odd; rewrite Rabs_Ropp. apply (cn_maj (S n) (S N)); lia. apply Rle_Rinv; INR_solve. unfold d', d; rewrite Ropp_Ropp_IZR; rewrite <- INR_IZR_INZ. rewrite <- Rabs_Ropp; rewrite Ropp_inv_permute. replace (- (2 * - INR (S n) + 1)) with ((2 * INR n + 1)) by (rewrite plus_1_S; ring). rewrite Rabs_pos_eq; try apply Rle_Rinv; try (apply Rlt_le; apply Rinv_0_lt_compat); INR_solve. rewrite INR_IZR_INZ; discrR. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith