proposition: Lemma bnz_bntg : forall n, bntg n = bnz (Z_of_nat n).
proof: Proof. intro n. unfold bntg, bnz. destruct n. simpl; field. rewrite <- INR_IZR_INZ. field. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith