proposition: Lemma mxrank_sum_cap m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (\rank (A + B) + \rank (A :&: B) = \rank A + \rank B)%N.
proof: Proof. set C := (A :&: B)%MS; set D := (A :\: B)%MS. have rDB: \rank (A + B)%MS = \rank (D + B)%MS. apply/eqP; rewrite mxrank_leqif_sup; first by rewrite addsmxS ?diffmxSl. by rewrite addsmx_sub addsmxSr -(addsmx_diff_cap_eq A B) addsmxS ?capmxSr. rewrite {1}rDB mxrank_disjoint_sum ?capmx_diff //. by rewrite addnC addnA mxrank_cap_compl. 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)