proposition: Lemma scalar_diag_block_mx c s (F : forall n, nat -> 'M_n.+1) : s != [::] -> (forall i, i < size s -> F (nth 0%N s i) i = c%:M ) -> diag_block_mx s F = c%:M.
proof: Proof. case: s => // x s _. elim: s x F=> /= [a F Hi| b l IHl a F Hi]. exact: (Hi 0%N). rewrite (Hi 0%N) // IHl -?scalar_mx_block // => i Hi2. exact: (Hi i.+1). 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