proposition: Lemma Frobenius_seqE n (A : 'M[F]_n) : Frobenius_seq A = nseq (n - size (invariant_factors A)) 1 ++ invariant_factors A.
proof: Proof. set m := subn _ _. have HfA:= (size_Frobenius_seq A). have Hfrob: sorted (@dvdpm F) (Frobenius_seq A). have Hdvd: {in (Frobenius_seq A) &, forall p q, dvdp p q -> dvdpm p q}. move=> p q /= /monic_Frobenius_seq Hp /monic_Frobenius_seq Hq H. by rewrite /dvdpm Hp Hq H. by apply/(sorted_trans Hdvd)/sorted_Frobenius_seq. have Hst: sorted (@dvdpm F) (nseq m 1 ++ invariant_factors A). apply: (@path_sorted _ _ 1); rewrite cat_path; apply/andP; split. apply/(pathP 0); rewrite size_nseq=> [][|i] Hi. by rewrite nth0 dvd1pm // nth_nseq Hi monic1. rewrite -nth_behead nth_nseq (ltn_trans (ltnSn i) Hi) dvd1pm //. by rewrite nth_nseq Hi monic1. rewrite path_min_sorted; [|apply/allP=>p Hp]. by rewrite sorted_filter //;first exact: dvdpm_trans. rewrite -nth_last nth_nseq size_nseq. by case: (m.-1 < m)%N; rewrite dvd1pm //; apply: (monic_invariant_factors Hp). apply: (sorted_eq (@dvdpm_trans F) (@dvdpm_asym F) Hfrob Hst). pose a:= fun p : E => (size p <= 1)%N. have HaC: {in (Frobenius_seq A), (fun p : E => (1 < size p)%N) =1 (predC a)}. by move=> p /=; rewrite -ltnNge. have Hfi: (invariant_factors A) = filter (predC a) (Frobenius_seq A). by rewrite -(eq_in_filter HaC). have Hm: m = size (filter a (Frobenius_seq A)). rewrite /m Hfi !size_filter. apply/eqP; rewrite -(eqn_add2r (count (predC a) (Frobenius_seq A))). by apply/eqP; rewrite subnK ?count_predC // -{2}HfA count_size. have Hfn: nseq m 1 = filter a (Frobenius_seq A). apply: (@eq_from_nth _ 0)=> [|i]; first by rewrite size_nseq. rewrite size_nseq => Hi; rewrite nth_nseq Hi. have: (filter a (Frobenius_seq A))`_i \in (filter a (Frobenius_seq A)). by rewrite mem_nth // -Hm. rewrite mem_filter=> /andP [Ha1 Ha2]. move: (monicP (monic_Frobenius_seq Ha2)). by rewrite (size1_polyC Ha1) lead_coefC => ->. by rewrite perm_sym Hfn Hfi; apply/permPl/perm_filterC. 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)