proposition: Lemma sorted_Frobenius_seq n (A : 'M[F]_n) : sorted (@dvdp _) (Frobenius_seq A).
proof: Proof. case: n A=> // n A. have Hp: forall (p : E), ((lead_coef p)^-1 *: p %= p)%P. move=> p; have [-> | p0] := eqVneq p 0; first by rewrite scaler0 eqpxx. apply/eqpP; exists ((lead_coef p),1). by rewrite oner_neq0 andbT lead_coef_eq0. rewrite scalerA mulrV ?scale1r //. by rewrite unitfE lead_coef_eq0. suff : sorted (@dvdr _) (Frobenius_seq A). by apply: sorted_trans=> x y _ _; rewrite dvdr_dvdp=> ->. have /mono_sorted it : {mono (fun p : {poly F} => (lead_coef p)^-1 *: p) : x y / x %| y}. by move=> x y; rewrite !dvdr_dvdp (eqp_dvdl _ (Hp x)) (eqp_dvdr _ (Hp y)). rewrite it. set s := Smith_seq _. apply/(sorted_take (@dvdr_trans _))/sorted_Smith. 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)