proposition: Lemma shift_polyE c p: p \shift c = \poly_(i < size p) \sum_(k < size p) p`_k * c ^+ (k - i) *+ 'C(k, i).
proof: Proof. rewrite /shift_poly comp_polyE poly_def; symmetry. transitivity (\sum_(i < size p) \sum_(k < size p) ((p`_k)%:P * (c ^+ (k - i) *+ 'C(k, i) *: 'X^i))). apply: eq_big => // [[i ip]] _ /=; rewrite - mul_polyC. rewrite rmorph_sum big_distrl; apply: eq_big => // [[k kp]] _ /=. rewrite - mulrnAr polyCM -mul_polyC mulrA //. rewrite exchange_big; apply: eq_big => // [[i ip]] _ /=. rewrite -big_distrr - mul_polyC; congr (_ * _). rewrite power_monom poly_def /=. have aux: forall j, (i < j < size p)%N ->(c ^+ (i - j) *+ 'C(i, j)) *: 'X^j = 0. move=> j; case /andP => ij js; rewrite bin_small ?mulr0n ? scale0r//. by rewrite (shorten_sum _ ip aux). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)