proposition: Lemma comm_coef_poly p x : comm_coef p x -> comm_poly p x.
proof: Proof. move=> cpx; rewrite /comm_poly !horner_coef big_distrl big_distrr /=. by apply: eq_bigr => i _; rewrite /= mulrA -cpx -!mulrA commrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)