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