proposition: Lemma shift_poly_is_linear c: linear (shift_poly c).
proof: Proof. by move=> a u v; rewrite /shift_poly comp_polyD comp_polyZ. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)