proposition: Lemma seq_exists : {q : IR | [0] [<=] q | q [<] [1] and (forall p : cpoly CC, monic n p -> forall c : IR, AbsCC p ! [0] [<] c -> {s : nat -> CC | forall i, AbsCC p ! (s i) [<=] q[^]i[*]c /\ AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*]c})}.
proof: Proof. elim (Kneser n lt0n). intros q; intros H H0. exists q. assumption. inversion_clear H0. rename X0 into H2. split. assumption. intros p mp c pzltc. exists (sK q H2 p mp c pzltc). split. exact (sK_prop1 q H2 p mp c pzltc i). exact (sK_prop2 q H2 p mp c pzltc i). Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)