proposition: Lemma bntg_neg_simpl : forall n, 1 / (- 2 * (INR n) + 1) ^ 2 = 1 / (2 * (INR n) - 1) ^ 2.
proof: Proof. intros; field. split. apply neg_odd_not_zero. replace (-2 * INR n + 1) with (- (2 * (INR n) - 1)) by field. apply Ropp_neq_0_compat; apply neg_odd_not_zero. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia