proposition: Lemma horner_exp_comm p x n : comm_poly p x -> (p ^+ n).[x] = p.[x] ^+ n.
proof: Proof. move=> comm_px; elim: n => [|n IHn]; first by rewrite hornerC. by rewrite !exprSr -IHn hornerM_comm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)