proposition: Fact degree_mxminpoly_proof : exists d, \rank (powers_mx A d.+1) <= d.
proof: Proof. by exists (n ^ 2)%N; rewrite rank_leq_col. 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)