proposition: Lemma mxrank_disjoint_sum m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :&: B)%MS = 0 -> \rank (A + B)%MS = (\rank A + \rank B)%N.
proof: Proof. move=> AB0; pose Ar := row_base A; pose Br := row_base B. have [Afree Bfree]: row_free Ar /\ row_free Br by rewrite !row_base_free. have: (Ar :&: Br <= A :&: B)%MS by rewrite capmxS ?eq_row_base. rewrite {}AB0 submx0 -mxrank_eq0 capmxE mxrankMfree //. set Cr := col_mx Ar Br; set Crl := lsubmx _; rewrite mxrank_eq0 => /eqP Crl0. rewrite -(adds_eqmx (eq_row_base _) (eq_row_base _)) addsmxE -/Cr. suffices K0: kermx Cr = 0. by apply/eqP; rewrite eqn_leq rank_leq_row -subn_eq0 -mxrank_ker K0 mxrank0. move/eqP: (mulmx_ker Cr); rewrite -[kermx Cr]hsubmxK mul_row_col -/Crl Crl0. rewrite mul0mx add0r -mxrank_eq0 mxrankMfree // mxrank_eq0 => /eqP->. exact: row_mx0. 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)