proposition: Lemma bntg_shift_neg_compat : Rseq_shift bntg_neg == bntg.
proof: Proof. intro n. unfold Rseq_shift. unfold bntg. unfold bntg_neg. rewrite S_INR. simpl pow. field; split. INR_solve. replace (-2 * (INR n + 1) + 1) with (- (2 * (INR n) + 1)) by field. apply Ropp_neq_0_compat. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith