proposition: Lemma det_ublock n1 n2 Aul (Aur : 'M[R]_(n1, n2)) Adr : \det (block_mx Aul Aur 0 Adr) = \det Aul * \det Adr.
proof: Proof. elim: n1 => [|n1 IHn1] in Aul Aur *. have ->: Aul = 1%:M by apply/matrixP=> i []. rewrite det1 mul1r; congr (\det _); apply/matrixP=> i j. by do 2![rewrite !mxE; case: splitP => [[]|k] //=; move/val_inj=> <- {k}]. rewrite (expand_det_col _ (lshift n2 0)) big_split_ord /=. rewrite addrC big1 1?simp => [|i _]; last by rewrite block_mxEdl mxE simp. rewrite (expand_det_col _ 0) big_distrl /=; apply: eq_bigr=> i _. rewrite block_mxEul -!mulrA; do 2!congr (_ * _). by rewrite col'_col_mx !col'Kl raddf0 row'Ku row'_row_mx IHn1. 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)