proposition: Lemma abound_eq : forall n N, (O <= n)%nat -> (S n <= N)%nat -> / (INR (N - n)) * (/ (INR (2 * n + 1)) + / (INR (2 * n + 3))) = / (INR (2 * N + 1)) * (2 / (INR (2 * n + 1)) + / (INR (N - n))) + / (INR (2 * N + 3)) * (2 / (INR (2 * n + 3)) + / (INR (N - n))).
proof: Proof. intros. rewrite minus_INR. repeat rewrite plus_INR. repeat rewrite mult_INR. replace (INR 1) with 1 by trivial. replace (INR 2) with 2 by trivial. field; INR_solve. eapply Nat.le_trans. constructor 2; constructor. assumption. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith