proposition: Lemma FTA_monic : forall (p : cpoly CC) (n : nat), 0 < n -> monic n p -> {c : CC | p ! c [=] [0]}.
proof: Proof. intros p n H0n mon. generalize (seq_exists n H0n). intro H. elim H. intros q qnonneg Hq1. elim Hq1. intros qlt10 Hq2. generalize (Hq2 p mon). intro Hq3. cut ([0] [<] AbsCC p ! [0][+][1]). intro Hp. elim (Hq3 (AbsCC p ! [0][+][1])). intros s Hs. cut (forall i : nat, AbsCC (s (S i) [-]s i) [^]n [<=] q[^]i[*] (AbsCC p ! [0][+][1])). intro Hs2. cut (CC_Cauchy_prop s). intro Hs3. exists (LimCC (Build_CC_CauchySeq s Hs3)). apply CC_SeqLimit_uniq with (fun n : nat => p ! (s n)). exact (poly_pres_lim (fun x : CC => p ! x) (contin_polyCC p) (Build_CC_CauchySeq s Hs3)). generalize (seq_yields_zero q qnonneg qlt10 (AbsCC p ! [0][+][1]) Hp (fun n0 : nat => p ! (s n0))). intro H0. apply H0. intro i. generalize (Hs i). intro H1; inversion_clear H1; assumption. exact (seq_is_CC_Cauchy n H0n q qnonneg qlt10 (AbsCC p ! [0][+][1]) Hp s Hs2). intro i; generalize (Hs i); intro Ha; elim Ha; intros; assumption. exact (less_plusOne _ (AbsCC p ! [0])). apply zero_lt_posplus1. apply AbsCC_nonneg. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)