proposition: Lemma det_lblock : forall n1 n2 Aul All Alr, \det (block_mx Aul '0m All Alr : 'M_(n1 + n2)) === \det Aul * \det Alr.
proof: Proof. move=> n1 n2 Aul All Alr. by rewrite <- det_trmx, trmx_block, trmx0, det_ublock, !det_trmx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms