proposition: Lemma poly_linear_shifted : forall (a : R) (f : RX), {f' : RX | {f'' : R | f [=] (_X_[-]_C_ a) [*]f'[+]_C_ f''}}.
proof: Proof. intros. induction f0 as [| s f0 Hrecf0]; intros. exists (cpoly_zero R). exists ([0]:R). simpl in |- *. algebra. elim Hrecf0. intro g'. intros H. elim H. intro g''. intros H0. exists (_X_[*]g'[+]_C_ g''). exists (a[*]g''[+]s). astepl (_X_[*]f0[+]_C_ s). astepl (_X_[*] ((_X_[-]_C_ a) [*]g'[+]_C_ g'') [+]_C_ s). apply eq_symmetric_unfolded. cut (_C_ (a[*]g''[+]s) [=] _C_ a[*]_C_ g''[+]_C_ s). intro. astepl ((_X_[-]_C_ a) [*] (_X_[*]g'[+]_C_ g'') [+] (_C_ a[*]_C_ g''[+]_C_ s)). unfold cg_minus. ring. Step_final (_C_ (a[*]g'') [+]_C_ s). Qed.
imports: CoRN.algebra.CPoly_Degree CoRN.algebra.COrdFields2 Coq.Classes.Morphisms Coq.Sorting.Permutation