proposition: Lemma addsmx_diff_cap_eq m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B + A :&: B :=: A)%MS.
proof: Proof. apply/eqmxP; rewrite addsmx_sub capmxSl diffmxSl /=. set C := (A :\: B)%MS; set D := capmx_gen A B. suffices sACD: (A <= C + D)%MS. by rewrite (submx_trans sACD) ?addsmxS ?capmxE. have:= addsmx_compl_full D; rewrite /row_full addsmxE. case/row_fullP=> U /(congr1 (mulmx A)); rewrite mulmx1. rewrite -[U]hsubmxK mul_row_col mulmxDr addrC 2!mulmxA. set V := _ *m _ => defA; rewrite -defA; move/(canRL (addrK _)): defA => defV. suffices /submxP[W ->]: (V <= C)%MS by rewrite -mul_row_col addsmxE submxMl. rewrite diffmxE sub_capmx {1}defV -mulNmx addmx_sub 1?mulmx_sub //. by rewrite -capmxE capmxSl. 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)