proposition: Lemma Kneser_2 : forall (k : nat) (z : CC), 1 <= k -> k <= n -> let r := AbsCC z in let p_ := fun i => a i[*]r[^]i in AbsCC (Sum 0 n (fun i => b i[*]z[^]i)) [<=] AbsCC (b_0[+]b k[*]z[^]k) [+] (Sum 1 (pred k) p_[+]Sum (S k) n p_).
proof: Proof. intros. unfold p_, r in |- *. set (p_' := fun i : nat => b i[*]z[^]i) in *. apply leEq_wdl with (AbsCC (b_0[+]b k[*]z[^]k[+] (Sum 1 (pred k) p_'[+]Sum (S k) n p_'))); unfold p_' in |- *. apply leEq_transitive with (AbsCC (b_0[+]b k[*]z[^]k) [+]AbsCC (Sum 1 (pred k) p_'[+]Sum (S k) n p_')); unfold p_' in |- *. apply triangle. apply plus_resp_leEq_lft. apply leEq_transitive with (AbsCC (Sum 1 (pred k) p_') [+]AbsCC (Sum (S k) n p_')); unfold p_' in |- *. apply triangle. apply plus_resp_leEq_both. apply Kneser_2c. auto with arith. apply Kneser_2c. auto with arith. apply AbsCC_wd. apply eq_symmetric_unfolded. apply Kneser_2b. auto. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma