proposition: Lemma calc3 : forall N, (An N) * (An N) - Bn N = bisum (fun n => pow1 n / (d' n) * (cn n N)) N.
proof: Proof. intros. rewrite calc2. apply bisum_eq_compat; intros. unfold cn. rewrite <- bisum_scal_mult. apply bisum_eq_compat; intros. unfold zr. destruct (Z.eq_dec z z0); field; [ | split ]; try apply d_not_null. discrR; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith