proposition: Lemma FTA' : forall n (f : CCX), degree_le n f -> nonConst _ f -> {z : CC | f ! z [=] [0]}.
proof: Proof. intro n. induction n as [| n Hrecn]. unfold nonConst in |- *. unfold degree_le in |- *. intros f H H0. elim H0. clear H0. intro n. intros H0 H1. elim (eq_imp_not_ap _ _ _ (H _ H0) H1). unfold nonConst in |- *. intros f H H0. elim H0. clear H0. intro m'. intros H0 H1. elim (poly_apzero_CC f). intro c. intros H2. elim (FTA_1' f n H c H2). intro a. intros H3. elim H3. clear H3. intro b. intros H3. elim H3. clear H3. intro g. intros H3 H4. elim (O_or_S m'); intro y. elim y. clear y. intro m. intro y. rewrite <- y in H0. rewrite <- y in H1. cut (a[*]nth_coeff m g [#] [0] or b[*]nth_coeff (S m) g [#] [0]). intro H5. elim H5; clear H5; intros H5. cut (a [#] [0]). intro H6. exists ( [--]b[/] a[//]H6). astepl ((_C_ a[*]_X_[+]_C_ b) [*]g) ! ( [--]b[/] a[//]H6). astepl ((_C_ a[*]_X_[+]_C_ b) ! ( [--]b[/] a[//]H6) [*]g ! ( [--]b[/] a[//]H6)). astepl (((_C_ a[*]_X_) ! ( [--]b[/] a[//]H6) [+] (_C_ b) ! ( [--]b[/] a[//]H6)) [*] g ! ( [--]b[/] a[//]H6)). astepl (((_C_ a) ! ( [--]b[/] a[//]H6) [*]_X_ ! ( [--]b[/] a[//]H6) [+]b) [*] g ! ( [--]b[/] a[//]H6)). astepl ((a[*] ( [--]b[/] a[//]H6) [+]b) [*]g ! ( [--]b[/] a[//]H6)). rational. apply cring_mult_ap_zero with (nth_coeff m g). auto. elim (Hrecn g); auto. intro z. intros. exists z. astepl ((_C_ a[*]_X_[+]_C_ b) [*]g) ! z. astepl ((_C_ a[*]_X_[+]_C_ b) ! z[*]g ! z). Step_final ((_C_ a[*]_X_[+]_C_ b) ! z[*][0]). unfold nonConst in |- *. exists (S m). auto. apply cring_mult_ap_zero_op with b. auto. apply cg_add_ap_zero. astepl (nth_coeff (S m) f). auto. Step_final (nth_coeff (S m) ((_C_ a[*]_X_[+]_C_ b) [*]g)). rewrite <- y in H0. elim (Nat.lt_irrefl 0 H0). apply nth_coeff_ap_zero_imp with m'. auto. Qed.
imports: CoRN.fta.CPoly_Rev CoRN.fta.FTAreg