proposition: Lemma shift_polyXn c i: ('X^i \shift c) = ('X + c%:P)^+i.
proof: Proof. by rewrite (shift_polyX c 'X i) /shift_poly comp_polyX. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)