proposition: Lemma mxblockP A B : (forall i j, submxblock A i j = submxblock B i j) <-> A = B.
proof: Proof. split=> [eqAB|->//]; apply/matrixP=> s t; have /matrixP := eqAB (sig1 s) (sig1 t). by move=> /(_ (sig2 s) (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)