proposition: Lemma trmx_block : forall (Aul : 'M_(m1, n1)) Aur All (Alr : 'M_(m2, n2)), (block_mx Aul Aur All Alr)^T === block_mx Aul^T All^T Aur^T Alr^T.
proof: Proof. move=> Aul Aur All Alr. pose (block_mx Aul Aur All Alr). rewrite -/m. rewrite <- (block_mxKul Aul Aur All Alr). rewrite <- (block_mxKll Aul Aur All Alr) at 2. rewrite <- (block_mxKur Aul Aur All Alr) at 3. rewrite <- (block_mxKlr Aul Aur All Alr) at 4. by rewrite -> trmx_ulsub, trmx_llsub, trmx_ursub, trmx_lrsub, submxK; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms