proposition: Lemma FTA_1 : {f1 : CCX | {f2 : CCX | degree_le 1 f1 /\ degree_le n f2 /\ f [=] f1[*]f2}}.
proof: Proof. elim (FTA_reg' g n FTA_1b). intro g1. intros H H0. elim H0. clear H0. intro g2. intros H0 H1. cut (degree_le 1 g1). intro. cut (degree_le n g2). intro. exists (Shift [--]c (Rev 1 g1)). exists (Shift [--]c (Rev n g2)). split. apply Shift_degree_le. apply Rev_degree_le. split. apply Shift_degree_le. apply Rev_degree_le. cut (degree_le (1 + n) (g1[*]g2)). intro. cut (degree_le (1 + n) g). intro. cut (degree_le (1 + n) (Shift c f)). intro. astepl (Shift [--]c (Shift c f)). astepl (Shift [--]c (Rev (1 + n) (Rev (S n) (Shift c f)))). astepl (Shift [--]c (Rev (1 + n) g)). astepl (Shift [--]c (Rev (1 + n) (g1[*]g2))). Step_final (Shift [--]c (Rev 1 g1[*]Rev n g2)). exact FTA_1a. apply degree_le_wd with (g1[*]g2); algebra. apply degree_le_mult; auto. apply degree_imp_degree_le; auto. apply degree_imp_degree_le; auto. Qed.
imports: CoRN.fta.CPoly_Rev CoRN.fta.FTAreg