proposition: Lemma horner_mxK p : mx_inv_horner (horner_mx A p) = p %% p_A.
proof: Proof. rewrite {1}(Pdiv.IdomainMonic.divp_eq mxminpoly_monic p) rmorphD rmorphM /=. rewrite mx_root_minpoly mulr0 add0r. by rewrite -(poly_rV_K (size_mod_mxminpoly _)) horner_rVpolyK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)