proposition: Lemma horner_mx_conj m n p (V : 'M[F]_(n.+1, m.+1)) (f : 'M_m.+1) : row_free V -> stablemx V f -> horner_mx (conjmx V f) p = conjmx V (horner_mx f p).
proof: Proof. move=> V_free V_stab; rewrite/conjmx; elim/poly_ind: p => [|p c]. by rewrite !rmorph0 mulmx0 mul0mx. rewrite !(rmorphD, rmorphM)/= !(horner_mx_X, horner_mx_C) => ->. rewrite [_ * _]mulmxA [_ *m (V *m _)]mulmxA mulmxKpV ?horner_mx_stable//. apply: (row_free_inj V_free); rewrite [_ *m V]mulmxDl. pose stablemxE := (stablemxD, stablemxM, stablemxC, horner_mx_stable). by rewrite !mulmxKpV -?[V *m _ *m _]mulmxA ?stablemxE// mulmxDr -scalar_mxC. 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)