proposition: Lemma col'_eq m n j0 (A B : 'M_(m, n)) : col' j0 A = col' j0 B -> forall i, {in predC1 j0, A i =1 B i}.
proof: Proof. move=> /matrixP eqAB' i j /[!inE]/[1!eq_sym]/unlift_some[j' -> _]. by have /[!mxE] := eqAB' i j'. 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)