proposition: Lemma mxcolEblock {p : nat} {p_ : 'I_p -> nat} n (C_ : forall i, 'M[T]_(p_ i, n)) : (\mxcol_i C_ i) = castmx (erefl, big_ord1 _ (fun=> n)) (\mxblock_(i < p, j < 1) C_ i).
proof: Proof. by apply: trmx_inj; rewrite tr_mxcol mxrowEblock trmx_cast tr_mxblock. 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 countalg finalg zmodp)