proposition: Lemma block_diag_mx_unit (R : comUnitRingType) n1 n2 (Aul : 'M[R]_n1) (Adr : 'M[R]_n2) : (block_mx Aul 0 0 Adr \in unitmx) = (Aul \in unitmx) && (Adr \in unitmx).
proof: Proof. by rewrite !unitmxE det_ublock unitrM. 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)