proposition: Lemma invmx_block_diag (R : comUnitRingType) n1 n2 (Aul : 'M[R]_n1) (Adr : 'M[R]_n2) : block_mx Aul 0 0 Adr \in unitmx -> invmx (block_mx Aul 0 0 Adr) = block_mx (invmx Aul) 0 0 (invmx Adr).
proof: Proof. move=> /[dup] Aunit; rewrite block_diag_mx_unit => /andP[Aul_unit Adr_unit]. rewrite -[LHS]mul1mx; apply: (canLR (mulmxK _)) => //. rewrite [RHS](mulmx_block (invmx Aul)) !(mulmx0, mul0mx, add0r, addr0). by rewrite !mulVmx// -?scalar_mx_block. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)