proposition: Lemma unitmx_diag_block s (F : forall n, nat -> 'M[R]_n.+1) : s != [::] -> (forall i, i < size s -> (F (nth 0%N s i) i) \in unitmx) -> (diag_block_mx s F) \in unitmx.
proof: Proof. case: s=> // a l _ H. have Ha: (F a 0%N) \in unitmx by exact: (H 0%N). elim: l a F Ha H=> //= b l IHl a F Ha H. rewrite unitmxE (det_ublock (F a 0%N)) unitrM -!unitmxE Ha /=. apply: IHl=> [|i]; first exact: (H 1%N). exact: (H 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