proposition: Lemma Kneser_2b : forall (k : nat) (z : CC), 1 <= k -> let p_ := fun i => b i[*]z[^]i in Sum 0 n (fun i => b i[*]z[^]i) [=] b_0[+]b k[*]z[^]k[+] (Sum 1 (pred k) p_[+]Sum (S k) n p_).
proof: Proof. intros. unfold p_ in |- *. unfold b_0 in |- *. apply eq_transitive_unfolded with (b 0[*]z[^]0[+]b k[*]z[^]k[+] (Sum 1 (pred k) p_[+]Sum (S k) n p_)); unfold p_ in |- *. apply Kneser_2a with (f := fun i : nat => b i[*]z[^]i). auto. rational. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma