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