proposition: Lemma FTA_1' : {a : CC | {b : CC | {g : CCX | degree_le n g | f [=] (_C_ a[*]_X_[+]_C_ b) [*]g}}}.
proof: Proof. elim FTA_1. intro f1. intros H. elim H. clear H. intros f2 H0. elim H0. clear H0. intro H. intros H0. elim H0. clear H0. intros H0 H1. elim (degree_le_1_imp _ f1); auto. intro a. intros H2. exists a. elim H2. clear H2. intro b. intros. exists b. exists f2. auto. Step_final (f1[*]f2). Qed.
imports: CoRN.fta.CPoly_Rev CoRN.fta.FTAreg