proposition: Lemma horner_mx_dvdp n (p q : {poly F}) (A : 'M_n.+1) : (dvdp p q) -> horner_mx A p = 0 -> horner_mx A q = 0.
proof: Proof. by case/dvdpP=> r ->; rewrite rmorphM=> /= ->; rewrite mulr0. Qed.
imports: mathcomp(all_ssreflect all_algebra)