proposition: Lemma shift_poly_nth1 c p i m: (size p <= m)%N -> (shift_poly c p)`_i = \sum_(k < m) p`_k * c^+(k - i) *+ 'C(k, i).
proof: Proof. move=> ltpm; rewrite shift_polyE coef_poly. case sip: (i < size p)%N; last first. rewrite big1 => // [[j jm]] _ /=; case (leqP i j) => ij. move: sip; case (ltnP i (size p)) => // sip1 _. by move: (leq_trans sip1 ij) => /(nth_default 0) ->; rewrite mul0r mul0rn. rewrite bin_small //. have aux: forall k, (size p <= k < m)%N ->p`_k * c ^+ (k - i) *+ 'C(k, i) = 0. move=> k; case /andP => ij js; move: ij => /(nth_default 0) ->. by rewrite mul0r mul0rn. symmetry;apply: (shorten_sum _ ltpm aux). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)