proposition: Lemma cn_pos : forall n N, (S n <= N)%nat -> cn (Zpos (P_of_succ_nat n)) N = (pow (-1) (S (S n))) * (sum_f_R0 (fun j => pow (-1) (j + N - n) * / (INR (j + N - n)))) (S (2 * n)) .
proof: Proof. intros. assert (odd' : forall a b, cn a b = - (cn (- a) b)) by (intros; rewrite cn_odd; ring). rewrite odd'. pose (N - S n)%nat as k. replace N with (k + S n)%nat by (unfold k; lia). unfold cn. replace (bisum (fun m : Z => if Z.eq_dec (- Zpos (P_of_succ_nat n)) m then 0 else pow1 m / IZR (m - - Zpos (P_of_succ_nat n))) (k + S n)) with (bisum (shiftp (fun j : Z => - (-1) ^ n * if Z.eq_dec 0 j then 0 else pow1 j / IZR j) (S n)) (k + S n)). rewrite bisum_shifting. assert (bisum (fun j : Z => - (-1) ^ n * (if Z.eq_dec 0 j then 0 else pow1 j / IZR j)) k = 0). induction k. simpl; ring. rewrite bisum_one_step. rewrite IHk. change (Z.eq_dec 0) with (Z.eq_dec (Z_of_nat O)). destruct (Z.eq_dec (Z_of_nat 0) (Z_of_nat (S k))). apply inj_eq_rev in e. inversion e. replace (Z.eq_dec (Z_of_nat O)) with (Z.eq_dec (- Z_of_nat O)%Z) by trivial. destruct (Z.eq_dec (- Z_of_nat O)%Z (- Z_of_nat (S k))). apply Z.opp_inj in e. apply inj_eq_rev in e. inversion e. ring_simplify. rewrite pow1_nat_neg. rewrite pow1_nat. rewrite Ropp_Ropp_IZR. field; discrR. rewrite H0; clear H0. rewrite Rplus_0_l. replace (mult 2 (S n)) with (S (S (2 * n))) by lia. rewrite sum_f_R0_sum1. assert (RE : forall x, - x = -1 * x) by (intro; ring); rewrite RE; clear RE. do 2 rewrite scal_sum. apply Rseq_sum_ext; intro i. unfold shiftp. replace (Z_of_nat (S i) + Z_of_nat k)%Z with (Z_of_nat (S i + k)). replace 0%Z with (Z_of_nat O) by trivial. destruct (Z.eq_dec (Z_of_nat O) (Z_of_nat (S i + k))). apply inj_eq_rev in e. inversion e. rewrite pow1_nat. rewrite <- INR_IZR_INZ. replace (i + (k + S n) - n)%nat with (S i + k)%nat by lia. simpl pow. field; INR_solve. simpl (S i + k)%nat. do 2 rewrite inj_S. rewrite Zplus_succ_l. inject. induction i. trivial. simpl (S i + k)%nat. do 2 rewrite inj_S. rewrite IHi. lia. apply bisum_eq_compat; intro. unfold shiftp. destruct (Z.eq_dec 0 (z + Z_of_nat (S n))); destruct (Z.eq_dec (- Zpos (P_of_succ_nat n)) z). auto with *. assert (z = - Z_of_nat (S n))%Z by lia. assert (- Zpos (P_of_succ_nat n) = (- Z_of_nat (S n)))%Z by trivial. subst; tauto. subst. assert (- Zpos (P_of_succ_nat n) = (- Z_of_nat (S n)))%Z by trivial. apply False_ind; lia. repeat rewrite <- Rmult_assoc. assert (AP : forall a b a' a'' b', a = a' * a'' -> b = b' -> (b' <> 0)%Z -> a' * (a'' / IZR b') = a / IZR b) by (intros; subst; field; discrR; auto); apply AP; clear AP; auto. rewrite pow1_plus_nat. ring_simplify. assert ((-1) ^ n * (-1) ^ S n = -1). rewrite <- Rdef_pow_add. replace (n + S n)%nat with (S (2 * n)) by lia. apply pow_1_odd. rewrite Rmult_assoc. rewrite H0. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith