proposition: Lemma row_eq m1 m2 n i1 i2 (A1 : 'M_(m1, n)) (A2 : 'M_(m2, n)) : row i1 A1 = row i2 A2 -> A1 i1 =1 A2 i2.
proof: Proof. by move/rowP=> eqA12 j; have /[!mxE] := eqA12 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)