proposition: Lemma col_eq m n1 n2 j1 j2 (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)) : col j1 A1 = col j2 A2 -> A1^~ j1 =1 A2^~ j2.
proof: Proof. by move/colP=> eqA12 i; have /[!mxE] := eqA12 i. 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)