proposition: Lemma shift_polyX c p i: ((p^+i) \shift c) = (p \shift c) ^+i.
proof: Proof. by rewrite /shift_poly - poly_comp_exp. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)