proposition: Lemma cn_odd : forall n N, cn (- n)%Z N = - (cn n N).
proof: Proof. intros. replace (- cn n N) with (-1 * cn n N) by ring. unfold cn. rewrite bisum_reverse. rewrite <- bisum_scal_mult. apply bisum_eq_compat; intros. unfold zr. destruct (Z.eq_dec (- n) (- z)); destruct (Z.eq_dec n z); subst; try ring. assert (n = z) by lia; subst; apply False_ind; apply n0; trivial. apply False_ind; apply n0; trivial. replace (- z - - n)%Z with (n - z)%Z by lia. replace (pow1 (- z)) with (pow1 z). replace (IZR (n - z)) with (- IZR (z - n)). field. discrR; lia. rewrite <- Ropp_Ropp_IZR; apply IZR_eq; lia. induction z; trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith