proposition: Lemma invmx_diag_block s (F : forall n, nat -> 'M[R]_n.+1) : (diag_block_mx s F) \in unitmx -> (diag_block_mx s F)^-1 = diag_block_mx s (fun n i => (F n i)^-1).
proof: Proof. case: s=> [|a l]; first by rewrite unitr0. elim: l a F => //= b l IHl a F H. rewrite invmx_block // IHl //. by move: H; rewrite !unitmxE (det_ublock (F a 0%N)) unitrM; case/andP. 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