proposition: Lemma genmx_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : <<A :&: B>>%MS = (<<A>> :&: <<B>>)%MS.
proof: Proof. rewrite -(eq_genmx (cap_eqmx (genmxE A) (genmxE B))). case idAB: (qidmx <<A>> || qidmx <<B>>)%MS. rewrite [@capmx]unlock !capmx_nop_id !(fun_if (@genmx _ _ _)) !genmx_id. by case: (qidmx _) idAB => //= ->. case idA: (qidmx _) idAB => //= idB; rewrite {2}capmx_eq_norm ?idA //. set C := (_ :&: _)%MS; have eq_idC: row_full C = qidmx C. rewrite qidmx_cap idA -sub1mx sub_capmx genmxE; apply/andP=> [[s1A]]. by case/idP: idA; rewrite qidmx_eq1 -genmx1 (sameP eqP genmxP) submx1. rewrite unlock /capmx_norm eq_idC. by apply: choose_id (capmx_witnessP _); rewrite -eq_idC 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)