proposition: Lemma capmxA m1 m2 m3 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) (C : 'M_(m3, n)) : (A :&: (B :&: C) = A :&: B :&: C)%MS.
proof: Proof. rewrite (capmxC A B) capmxC; wlog idA: m1 m3 A C / qidmx A. move=> IH; case idA: (qidmx A); first exact: IH. case idC: (qidmx C); first by rewrite -IH. rewrite (@capmx_eq_norm n m3) ?qidmx_cap ?idA ?idC ?andbF //. rewrite capmx_eq_norm ?qidmx_cap ?idA ?idC ?andbF //. apply: capmx_norm_eq; first by rewrite !qidmx_cap andbAC. by apply/andP; split; rewrite !sub_capmx andbAC -!sub_capmx. rewrite -!(capmxC A) [in @capmx _ m1]unlock idA capmx_nop_id. have [eqBC|] := eqVneq (qidmx B) (qidmx C). rewrite (@capmx_eq_norm n) ?capmx_nopP // capmx_eq_norm //. by apply: capmx_norm_eq; rewrite ?qidmx_cap ?capmxS ?capmx_nopP. by rewrite !unlock capmx_nopP capmx_nop_id; do 2?case: (qidmx _) => //. 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)