proposition: Lemma muls_eqmx m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) : (R1 :=: R3 -> R2 :=: R4 -> R1 * R2 = R3 * R4)%MS.
proof: Proof. move=> eqR13 eqR24; rewrite -(genmx_muls R1 R2) -(genmx_muls R3 R4). by apply/genmxP; rewrite !mulsmxS ?eqR13 ?eqR24. 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)