proposition: Lemma poly_linear_factor : forall (f : RX) a, f ! a [=] [0] -> {f' : RX | f [=] (_X_[-]_C_ a) [*]f'}.
proof: Proof. intros. elim (poly_linear_shifted a f0). intro f'. intros H0. elim H0. intro f''. intros H1. exists f'. cut (_C_ f'' [=] [0]). intro. astepl ((_X_[-]_C_ a) [*]f'[+]_C_ f''). Step_final ((_X_[-]_C_ a) [*]f'[+][0]). astepr (_C_ ([0]:R)). apply cpoly_const_eq. astepl ([0][+]f''). astepl ([0][*]f' ! a[+]f''). astepl ((a[-]a) [*]f' ! a[+]f''). astepl ((_X_ ! a[-] (_C_ a) ! a) [*]f' ! a[+]f''). astepl ((_X_[-]_C_ a) ! a[*]f' ! a[+]f''). astepl (((_X_[-]_C_ a) [*]f') ! a[+]f''). astepl (((_X_[-]_C_ a) [*]f') ! a[+] (_C_ f'') ! a). astepl ((_X_[-]_C_ a) [*]f'[+]_C_ f'') ! a. Step_final f0 ! a. Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation