proposition: Lemma eqmx_col {m} (V_ : forall i, 'M[F]_(p_ i, m)) : (\mxcol_i V_ i :=: \sum_i <<V_ i>>)%MS.
proof: Proof. apply/eqmxP/andP; split. apply/row_subP => i; rewrite row_mxcol. by rewrite (sumsmx_sup (sig1 i))// genmxE row_sub. apply/sumsmx_subP => i0 _; rewrite genmxE; apply/row_subP => j. apply: (eq_row_sub (Rank _ j)); apply/rowP => k. by rewrite !mxE Rank2K; case: _ / esym; rewrite cast_ord_id. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)