proposition: Lemma map_mulsmx m1 m2 n (E1 : 'A_(m1, n)) (E2 : 'A_(m2, n)) : ((E1 * E2)%MS^f :=: E1^f * E2^f)%MS.
proof: Proof. rewrite /mulsmx; elim/big_rec2: _ => [|i A Af _ eqA]; first by rewrite map_mx0. apply: (eqmx_trans (map_addsmx _ _)); apply: adds_eqmx {A Af}eqA. apply/eqmxP; rewrite !map_genmx !genmxE map_mxM. apply/rV_eqP=> u; congr (u <= _ *m _)%MS. by apply: map_lin_mx => //= A; rewrite map_mxM // map_vec_mx map_row. 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)