proposition: Lemma cast_col_mx m1 m2 n n' (eq_n : n = n') A1 A2 : castmx (erefl _, eq_n) (col_mx A1 A2) = col_mx (castmx (erefl m1, eq_n) A1) (castmx (erefl m2, eq_n) A2).
proof: Proof. by case: n' / eq_n. 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)