proposition: Lemma exp_diag_block_cons s F k : s != [::] -> (diag_block_mx s F)^+ k = diag_block_mx s (fun n i => (F n i)^+ k).
proof: Proof. case: s=> // x s _. elim: s x F => //= a l IHl x 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