proposition: Lemma FTA_reg' : {f1 : CCX | degree 1 f1 | {f2 : CCX | degree n f2 | f [=] f1[*]f2}}.
proof: Proof. elim (FTA_reg f (S n)). intro c. intro H. cut (degree 1 (_X_[-]_C_ c)). intro. exists (_X_[-]_C_ c). auto. elim (poly_linear_factor _ _ _ H). intro f2. intros. exists f2. apply degree_mult_imp with (_X_[-]_C_ c) 1. auto. apply degree_wd with f; auto. auto. apply degree_minus_lft with 0. apply degree_le_c_. apply degree_x_. auto. auto with arith. auto. Qed.
imports: CoRN.fta.CPoly_Rev CoRN.fta.FTAreg