proposition: Lemma kermxpoly_min n (g : 'M[K]_n.+1) p : mxminpoly g %| p -> (kermxpoly g p :=: 1)%MS.
proof: Proof. by rewrite /kermxpoly => /mxminpoly_minP ->; apply: kermx0. 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)