proposition: Lemma rank_mxdiag (V_ : forall i, 'M[F]_(p_ i)) : (\rank (\mxdiag_i V_ i) = \sum_i \rank (V_ i))%N.
proof: Proof. elim: {+}n {+}p_ V_ => [|m IHm] q_ V_. by move: (\mxdiag__ _); rewrite !big_ord0 => M; rewrite flatmx0 mxrank0. rewrite mxdiag_recl [RHS]big_ord_recl/= -IHm. by case: _ / mxsize_recl; rewrite ?castmx_id rank_diag_block_mx. 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)