proposition: Lemma eq_block_mx Aul Aur Adl Adr Bul Bur Bdl Bdr : block_mx Aul Aur Adl Adr = block_mx Bul Bur Bdl Bdr -> [/\ Aul = Bul, Aur = Bur, Adl = Bdl & Adr = Bdr].
proof: Proof. by case/eq_col_mx; do 2!case/eq_row_mx=> -> ->. 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)