proposition: Lemma hornerM_comm p q x : comm_poly q x -> (p * q).[x] = p.[x] * q.[x].
proof: Proof. move=> comm_qx. elim/poly_ind: p => [|p c IHp]; first by rewrite !(simp, horner0). rewrite mulrDl hornerD hornerCM -mulrA -commr_polyX mulrA hornerMX. by rewrite {}IHp -mulrA -comm_qx mulrA -mulrDl hornerMXaddC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)