proposition: Lemma monic_Frobenius_seq n (A : 'M[F]_n) p: p \in Frobenius_seq A -> p \is monic.
proof: Proof. move=> Hp. have := Frobenius_seq_neq0 Hp. move: Hp; rewrite /Frobenius_seq=> /(nthP 0) []i. rewrite size_map=> Hi; rewrite (nth_map 0) // => <-. rewrite scaler_eq0 negb_or=> /andP [_ H0]. by apply: monic_leadVMp; rewrite unitfE lead_coef_eq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image companion closed_poly smith_complements)