proposition: Lemma equiv_sbc_ssc n (A : 'M[F]_n) : equivalent (Smith_block_cpmx A) (Smith_seq_cpmx A).
proof: Proof. rewrite /Smith_block_cpmx /Smith_seq_cpmx Frobenius_seqE. have: forall p, p \in invariant_factors A -> (0 < (size p).-1)%N. by move=> p; rewrite mem_filter -subn1 subn_gt0=> /andP []. rewrite -{10}(sum_size_inv_factors A). case: (invariant_factors A)=> [_|a l]. by rewrite big_nil diag_mx_seq_nil; exact: equiv_refl. elim: l a=> /= [a Hp|b l IHl a Hp]. by rewrite big_cons big_nil addn0 subn1 cats1; exact: equiv_refl. have IHp : forall p : E, p \in b :: l -> (0 < (size p).-1)%N. by move=> p H; apply: Hp; rewrite mem_behead. have Ha: (0 < (size a).-1)%N by rewrite Hp // mem_head. have Hb: (0 < (size b).-1)%N by rewrite IHp // mem_head. set M := diag_mx_seq _ _ _. apply: (equiv_trans (equiv_drblockmx M (IHl b IHp))). rewrite -diag_mx_seq_cat ?size_rcons ?size_nseq //. set s2 := [seq (size p).-2 | p : E <- (b :: l)]. set k := (\sum_(_ <- _) _)%N. set m := (\sum_(_ <- _) _)%N. have Hk: k = (size_sum s2).+1. rewrite size_sum_big_cons /k !big_cons !big_map /= prednK //. congr (_ + _)%N; apply: eq_big_seq=> i Hi. by rewrite (@prednK (size i).-1) // IHp // mem_behead. have Hltk : (size l < k)%N. rewrite /k (eq_big_seq (fun p : E => (size p).-2 + 1)%N). rewrite big_split /= addnC (big_nth 0) sum_nat_const_nat. by rewrite subn0 muln1 leq_addr. by move=> i Hi /=; rewrite addn1 prednK // IHp. apply/similar_equiv/similar_diag_mx_seq=> //. by rewrite !size_cat size_rcons !size_nseq subnK // Hk. apply/seq.permP=> x /=. rewrite -cats1 !count_cat /= !count_nseq. rewrite !addnA addn0 (addnAC _ (x a)) -mulnDr; congr (_ * _ + _ + _ + _)%N. by rewrite /m big_cons (subnS _ (size l).+1) -{2}(prednK Ha) -addnBA //. 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)