proposition: Lemma scaleS (p : {poly R}) (u v : R) : (p \scale u) \scale v = p \scale (u * v).
proof: Proof. rewrite /scaleX_poly -comp_polyA comp_polyM !comp_polyC comp_polyX. by rewrite -mulrA -polyCM [v * u]mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc