proposition: Lemma sub_kermxpoly_conjmx V f p W : stablemx V f -> row_free V -> (W <= kermxpoly (conjmx V f) p)%MS = (W *m V <= kermxpoly f p)%MS.
proof: Proof. case: n m => [|n'] [|m'] in V f W * => fV rfV; rewrite ?thinmx0//. by rewrite /row_free mxrank.unlock in rfV. by rewrite mul0mx !sub0mx. apply/sub_kermxP/sub_kermxP; rewrite horner_mx_conj//; last first. by move=> /(congr1 (mulmxr (pinvmx V)))/=; rewrite mul0mx !mulmxA. move=> /(congr1 (mulmxr V))/=; rewrite ![W *m _]mulmxA ?mul0mx mulmxKpV//. by rewrite -mulmxA mulmx_sub// horner_mx_stable//. 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)