proposition: Lemma rank_diag_block_mx m n p q (A : 'M_(m, n)) (B : 'M_(p, q)) : \rank (block_mx A 0 0 B) = (\rank A + \rank B)%N.
proof: Proof. rewrite block_mxEv -addsmxE mxrank_disjoint_sum ?rank_row_mx0 ?rank_row_0mx//. apply/eqP/rowV0P => v; rewrite sub_capmx => /andP[/submxP[x ->]]. rewrite mul_mx_row mulmx0 => /submxP[y]; rewrite mul_mx_row mulmx0. by move=> /eq_row_mx[-> _]; rewrite 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)