proposition: Lemma pi_tg2_corresp : forall n, pi_tg2 n = tg_alt PI_tg (2 * n) + tg_alt PI_tg (S (2 * n)).
proof: Proof. intros. unfold tg_alt, PI_tg, pi_tg2. rewrite pow_1_odd. rewrite pow_1_even. assert (R1 : INR ((2 * (2 * n) + 1)%nat) = 2 * (2 * (INR n)) + 1) by INR_solve. assert (R2 : INR ((2 * S (2 * n) + 1)%nat) = 2 * (1 + (2 * (INR n))) + 1) by INR_solve. rewrite R1. rewrite R2. field. split; [replace (1 + 2 * (INR n)) with (INR (1 + 2 * n)); [apply (odd_not_zero) | rewrite plus_INR] |replace (2 * (INR n)) with (INR (2 * n)); [apply odd_not_zero | ]]; rewrite mult_INR; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia