proposition: Lemma mxrowP m (A B : 'M_(m, sq)) : (forall j, submxrow A j = submxrow B j) <-> A = B.
proof: Proof. split=> [eqAB|->//]; apply/matrixP=> i t; have /matrixP := eqAB (sig1 t). by move=> /(_ i (sig2 t)); rewrite !mxE !sig2K. 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)