proposition: Lemma Kneser : forall n : nat, 0 < n -> {q : IR | [0] [<=] q | q [<] [1] and (forall p : cpoly CC, monic n p -> forall c : IR, AbsCC p ! [0] [<] c -> {z : CC | AbsCC z[^]n [<=] c | AbsCC p ! z [<] q[*]c})}.
proof: Proof. intros n H. exists ([1][-]p3m n[*]p3m (2 * n * n)). apply less_leEq. apply less_leEq_trans with (Half:IR). apply pos_half. apply Kneser_1'; auto. split. apply Kneser_1''. intros p H0 c H1. elim H0. intros H2 H3. cut (nth_coeff n p [=] [1]). intro H4. 2: auto. elim (Kneser_3 (fun i : nat => nth_coeff i p) n H H4 c). intros z H6 H7. 2: astepl (AbsCC p ! [0]); auto. exists z. auto. astepl (AbsCC (Sum 0 n (fun i : nat => nth_coeff i p[*]z[^]i))); auto. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma