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