proposition: Lemma horner_scaleX_poly c p x : (p \scale c).[x] = p.[c * x].
proof: Proof. by rewrite horner_comp ! hornerE mulrC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)