proposition: Lemma exp_diag_block_S s F k : (diag_block_mx s F)^+ k.+1 = diag_block_mx s (fun n i => (F n i)^+ k.+1).
proof: Proof. case: s=>[|a l]; first by rewrite expr0n /=. elim: l a F=> //= b l IHl a F. by rewrite -IHl exp_block_mx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring