proposition: Lemma pminor_char_poly_mx_monic m p (M : 'M[R]_m) (h h': p.+1 <= m) : pminor h h' (char_poly_mx M) \is monic.
proof: Proof. have h'h : widen_ord h' =1 widen_ord h by apply/widen_ord_eq. rewrite /pminor (minor_eq (frefl _) h'h) /minor submatrix_char_poly_mx. by rewrite char_poly_monic. exact: inj_widen_ord. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)