proposition: Lemma shift_poly_multiplicative c: multiplicative (shift_poly c).
proof: Proof. split. move=> x y; exact: comp_polyM. by rewrite /shift_poly comp_polyC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)