proposition: Lemma capmxC m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B = B :&: A)%MS.
proof: Proof. have [eqAB|] := eqVneq (qidmx A) (qidmx B). rewrite (capmx_eq_norm eqAB) (capmx_eq_norm (esym eqAB)). apply: capmx_norm_eq; first by rewrite !qidmx_cap andbC. by apply/andP; split; rewrite !sub_capmx andbC -sub_capmx. by rewrite negb_eqb !unlock => /addbP <-; case: (qidmx A). 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)