Shifting polynomials

This can be done for CRings in general, but we do it here only for C because extensionality makes everything much easier, and we only need it for C.

Section Poly_Shifted.

Definition Shift (a : C) (p : C[X]) :=
∑ 0 (lth_of_poly p) (fun i => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i).

Lemma Shift_apply : forall a p (x : C), (Shift a p) ! x [=] p ! (x[+]a).

Lemma Shift_wdr : forall a p p', p [=] p' -> Shift a p [=] Shift a p'.

Lemma Shift_shift : forall a p, Shift [--]a (Shift a p) [=] p.

Lemma Shift_mult : forall a p1 p2, Shift a (p1[*]p2) [=] Shift a p1[*]Shift a p2.

Lemma Shift_degree_le : forall a p n, degree_le n p -> degree_le n (Shift a p).

Lemma Shift_monic : forall a p n, monic n p -> monic n (Shift a p).

End Poly_Shifted.