proposition: Lemma map_col_base m n (A : 'M_(m, n)) : (col_base A)^f = castmx (erefl m, mxrank_map A) (col_base A^f).
proof: Proof. move: (mxrank_map A); rewrite {2}/col_base mxrank_map => eqrr. by rewrite castmx_id map_mxM map_pid_mx map_col_ebase. 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)