proposition: Lemma shift_poly_nth p i c: (i < size p)%N -> (shift_poly c p)`_i = \sum_(k < size p) p`_k * c^+(k - i) *+ 'C(k, i).
proof: Proof. by move=> ltis; rewrite shift_polyE coef_poly ltis. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)