proposition: Lemma exp_block_mx m n (A: 'M[R]_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]. by rewrite !expr0 -scalar_mx_block. rewrite !exprS IHk /GRing.mul /= (mulmx_block A 0 0 B (A ^+ k)). by rewrite !mulmx0 !mul0mx !add0r !addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)