proposition: Lemma horner_rVpolyK (u : 'rV_d) : mx_inv_horner (horner_mx A (rVpoly u)) = rVpoly u.
proof: Proof. congr rVpoly; rewrite horner_rVpoly vec_mxK. by apply: (row_free_inj minpoly_mx_free); rewrite mulmxKpV ?submxMl. 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)