proposition: Lemma exp_block_diag_mx m n (A: 'M_m.+1) (B : 'M_n.+1) k : (block_mx A 0 0 B) ^+ k = block_mx (A ^+ k) 0 0 (B ^+ k).
proof: Proof. elim: k=> [|k IHk]; first by rewrite !expr0 -scalar_mx_block. rewrite !exprS IHk [LHS](mulmx_block A _ _ _ (A ^+ k)). by rewrite !mulmx0 !mul0mx !add0r !addr0. 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 countalg finalg zmodp)