proposition: Lemma eq_genmx m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :=: B -> <<A>> = <<B>>)%MS.
proof: Proof. move=> eqAB; rewrite unlock. have{} eqAB: equivmx A (row_full A) =1 equivmx B (row_full B). by move=> C; rewrite /row_full /equivmx !eqAB. rewrite (eq_choose eqAB) (choose_id _ (genmx_witnessP B)) //. by rewrite -eqAB genmx_witnessP. 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 finalg zmodp matrix)