proposition: Lemma invmx_block n1 n2 (Aul : 'M[R]_n1.+1) (Adr : 'M[R]_n2.+1) : (block_mx Aul 0 0 Adr) \in unitmx -> (block_mx Aul 0 0 Adr)^-1 = block_mx Aul^-1 0 0 Adr^-1.
proof: Proof. move=> Hu. have Hu2: (block_mx Aul 0 0 Adr) \is a GRing.unit by []. rewrite unitmxE det_ublock unitrM in Hu. case/andP: Hu; rewrite -!unitmxE => HAul HAur. have H: block_mx Aul 0 0 Adr * block_mx Aul^-1 0 0 Adr^-1 = 1. rewrite /GRing.mul /= (mulmx_block Aul _ _ _ Aul^-1) !mulmxV //. by rewrite !mul0mx !mulmx0 !add0r addr0 -scalar_mx_block. by apply: (mulrI Hu2); rewrite H mulrV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype finfun perm matrix bigop zmodp mxalgebra) mathcomp(choice poly polydiv mxpoly binomial)