proposition: Lemma commr_horner a b p : GRing.comm a b -> comm_coef p a -> GRing.comm a p.[b].
proof: Proof. move=> cab cpa; rewrite horner_coef; apply: commr_sum => i _. by apply: commrM => //; apply: commrX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)