proposition: Lemma horner_mx_uconj n p (V : 'M[F]_(n.+1)) (f : 'M_n.+1) : V \is a GRing.unit -> horner_mx (V *m f *m invmx V) p = V *m horner_mx f p *m invmx V.
proof: Proof. move=> V_unit; rewrite -!conjumx//. by rewrite horner_mx_conj ?row_free_unit ?stablemx_unit. 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)