proposition: Lemma FTA_reg : forall (p : cpoly CC) (n : nat), 0 < n -> degree n p -> {c : CC | p ! c [=] [0]}.
proof: Proof. intros p n H H0. elim (FTA_monic (poly_norm _ p n H0) n); auto. intros. exists x. apply poly_norm_apply with n H0; auto. apply poly_norm_monic; auto. Qed.
imports: CoRN.fta.KneserLemma CoRN.fta.CPoly_Shift CoRN.fta.CPoly_Contin1 Coq(Lia)