proposition: Lemma Frobenius n (A : 'M[F]_n.+1) : similar A (Frobenius_form A).
proof: Proof. apply/similar_fundamental; rewrite char_diag_block_mx; last first. by rewrite -size_eq0 size_map size_eq0 nnil_inv_factors. apply: (equiv_trans (equiv_Smith (char_poly_mx A))). rewrite /Smith_form. apply/(equiv_trans (equiv_Frobenius_seq A))/equiv_sym. have Hn := size_Frobenius_seq A. rewrite /equivalent -{2 4 37 38 43 44}Hn cast_inv. apply: (equiv_trans _ (equiv_sbc_ssc A)). apply: equiv_diag_block=>[|i]; first by rewrite !size_map. rewrite size_map=> Hi. rewrite !(nth_map 0) //. set C := char_poly_mx _. apply: (equiv_trans (equiv_Smith C)). apply: Smith_companion; move: (mem_nth 0 Hi). by rewrite mem_filter=> /andP []. exact: monic_invariant_factors. 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)