proposition: Lemma pminor_char_poly_mx_monic: forall m p (M: 'M[R]_m) (h h': p.+1 <= m), pminor h h' (char_poly_mx M) \is monic.
proof: Proof. rewrite /pminor => m p M h h'. rewrite (@minor_eq _ _ _ _ _ (widen_ord h) _ (widen_ord h)); first last. - by apply: widen_ord_eq. - by move => x. rewrite /minor submatrix_char_poly_mx; last by apply: inj_widen_ord. by apply/char_poly_monic. Qed.
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