proposition: Lemma hornerCM a p x : (a%:P * p).[x] = a * p.[x].
proof: Proof. elim/poly_ind: p => [|p c IHp]; first by rewrite !(mulr0, horner0). by rewrite mulrDr mulrA -polyCM !hornerMXaddC IHp mulrDr mulrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)