proposition: Lemma scaleX_polyE c p: p \scale c = \poly_(i < size p)(p`_i * c ^+i).
proof: Proof. rewrite /scaleX_poly comp_polyE poly_def; apply: eq_bigr => i _. by rewrite -scalerA - exprZn - (mul_polyC c) commr_polyX. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)