proposition: Lemma cast_inv n (A : 'M[F]_n.+1) : size (Frobenius_seq A) = (size_sum [seq (size p).-2 | p : E <- invariant_factors A]).+1.
proof: Proof. rewrite size_Frobenius_seq -{1}(sum_size_inv_factors A). rewrite size_sum_big; last first. by rewrite -size_eq0 size_map size_eq0 nnil_inv_factors. rewrite !big_map /=; apply: eq_big_seq=> i. rewrite mem_filter=> /andP [Hi _]. by rewrite prednK // -subn1 subn_gt0. 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)