fact: Definition char_poly_alt n (M: 'M[R]_(1 + n)) := bareiss (char_poly_mx M : 'M[polydvd.poly_of R]__).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice matrix bigop zmodp poly polydiv mxpoly) CoqEAL(ssrcomplements minor dvdring) polydvd