proposition: Lemma shift_poly_scal a b p : (a%:P * p) \shift b = a%:P * (p \shift b).
proof: Proof. by rewrite shift_poly_multiplicative shift_polyC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)