fact: Definition block_mx Aul Aur All Alr : 'M_(m1 + m2, n1 + n2) := (pastemx (pastemx Aul Aur)^T (pastemx All Alr)^T)^T.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms