proposition: Lemma calc1 : forall N, (An N) * (An N) - Bn N = bisumsum_strip_diag' (fun n m => (pow1 m * pow1 n) * / (2 * (IZR (m - n))) * (/ (d' n) - / (d' m)) ) N.
proof: Proof. assert (forall z, 2 * IZR z + 1 <> 0) by (intro; discrR; lia). intros N. unfold An. rewrite <- bisumsum_square. replace (Bn N) with (bisum (fun i => anz i * anz i) N). rewrite bisumsum_strip_diag'_eq_but_diag_compat with _ (fun i j => anz i * anz j) _. rewrite strip_diag. unfold bisumsum_strip_diag. trivial. intros. unfold anz. replace (pow1 i / (2 * IZR i + 1) * (pow1 j / (2 * IZR j + 1))) with (pow1 i * pow1 j * (/ ((2 * IZR i + 1) * (2 * IZR j + 1)))). 2:field_simplify; [ trivial | split | split ]; try apply d_not_null. replace (2 * IZR i + 1) with (d (IZR i)) by trivial. replace (2 * IZR j + 1) with (d (IZR j)) by trivial. rewrite splitmn; try apply d_not_null; try (discrR; lia). unfold d'. rewrite Z_R_minus. field; repeat split; try apply d_not_null; discrR; lia. apply bisum_eq_compat. intro. unfold bnz, anz; field_simplify; try apply H. rewrite pow1_squared; field. unfold pow. discrR; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith