proposition: Lemma col_mxA m1 m2 m3 n (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)) (A3 : 'M_(m3, n)) : let cast := (esym (addnA m1 m2 m3), erefl n) in col_mx A1 (col_mx A2 A3) = castmx cast (col_mx (col_mx A1 A2) A3).
proof: Proof. by apply: trmx_inj; rewrite trmx_cast !tr_col_mx -row_mxA. 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)