proposition: Lemma eqmxP m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : reflect (A :=: B)%MS (A == B)%MS.
proof: Proof. apply: (iffP andP) => [[sAB sBA] | eqAB]; last by rewrite !eqAB. split=> [|m3 C]; first by apply/eqP; rewrite eqn_leq !mxrankS. split; first by apply/idP/idP; apply: submx_trans. by apply/idP/idP=> sC; apply: submx_trans sC _. 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)