Section FTA_reg'.
Variable f : cpoly_cring C.
Variable n : N.
Hypothesis f_degree : degree (S n) f.
Lemma FTA_reg' : {f1 : C[X] | degree 1 f1 | {f2 : C[X] | degree n f2 | f [=] f1[*]f2}}.
End FTA_reg'.
Let n:nat, f be a complex polynomial of degree
less than or equal to (S n) and c be a complex number such that
f!c [#] 0.
Section FTA_1.
Variable f : cpoly_cring C.
Variable n : N.
Hypothesis f_degree : degree_le (S n) f.
Variable c : C.
Hypothesis f_c : f ! c [#] 0.
Lemma FTA_1a : degree_le (S n) (Shift c f).
Let g := Rev (S n) (Shift c f).
Lemma FTA_1b : degree (S n) g.
Lemma FTA_1 : {f1 : C[X] | {f2 : C[X] | degree_le 1 f1 /\ degree_le n f2 /\ f [=] f1[*]f2}}.
Lemma FTA_1' : {a : C | {b : C | {g : C[X] | degree_le n g | f [=] (_C_ a[*]_X_[+]_C_ b) [*]g}}}.
End FTA_1.
Section Fund_Thm_Alg.
Lemma FTA' : forall n (f : C[X]), degree_le n f -> nonConst _ f -> {z : C | f ! z [=] 0}.
Lemma FTA : forall f : C[X], nonConst _ f -> {z : C | f ! z [=] 0}.
Lemma FTA_a_la_Henk : forall f : C[X],
{x : C | {y : C | AbsCC (f ! x[-]f ! y) [>]0}} -> {z : C | f ! z [=] 0}.
End Fund_Thm_Alg.