proposition: Lemma mxminpoly_nonconstant : d > 0.
proof: Proof. rewrite /d; case: ex_minnP => -[] //; rewrite leqn0 mxrank_eq0; move/eqP. by move/row_matrixP/(_ 0)/eqP; rewrite rowK row0 mxvec_eq0 -mxrank_eq0 mxrank1. 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)