proposition: Lemma Kneser_2c : forall (m n : nat) (z : CC), m <= S n -> let r := AbsCC z in AbsCC (Sum m n (fun i => b i[*]z[^]i)) [<=] Sum m n (fun i => a i[*]r[^]i).
proof: Proof. intros. unfold r in |- *. apply leEq_wdr with (Sum m n0 (fun i : nat => AbsCC (b i[*]z[^]i))). apply triangle_Sum with (z := fun i : nat => b i[*]z[^]i). auto. apply Sum_wd. intros. unfold a in |- *. Step_final (AbsCC (b i) [*]AbsCC (z[^]i)). Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma