proposition: Lemma calc2 : forall N, (An N) * (An N) - Bn N = bisumsum_strip_diag' (fun n m => (pow1 m * pow1 n) * / ((IZR (m - n)) * (d' n)) ) N.
proof: Proof. intros. rewrite calc1. rewrite bisumsum_strip_diag'_eq_but_diag_compat with _ (fun n m : Z => pow1 m * pow1 n / (2 * IZR (m - n)) * ( / d' n) + pow1 m * pow1 n / (2 * IZR (m - n)) * (- / d' m)) _. rewrite bisumsum_strip_diag'_plus. rewrite bisumsum_strip_diag'_switch_index. rewrite <- bisumsum_strip_diag'_plus. rewrite bisumsum_strip_diag'_switch_index. apply bisumsum_strip_diag'_eq_but_diag_compat. intros. replace (IZR (i - j)) with (- IZR (j - i)). field; split. apply d_not_null. discrR; lia. repeat rewrite <- Z_R_minus; ring. intros. field; repeat split. apply d_not_null. discrR; lia. apply d_not_null. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith