proposition: Lemma capmxE m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B :=: capmx_gen A B)%MS.
proof: Proof. rewrite unlock -sub1mx; apply/eqmxP. have:= submx_refl (capmx_gen A B); rewrite !sub_capmx_gen => /andP[sIA sIB]. case idA: (qidmx A); first by rewrite !capmx_nopP submx_refl sub_qidmx. case idB: (qidmx B); first by rewrite !capmx_nopP submx_refl sub_qidmx. case s1B: (1%:M <= B)%MS; rewrite !capmx_normP ?sub_capmx_gen sIA ?sIB //=. by rewrite submx_refl (submx_trans (submx1 _)). 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)