proposition: Lemma block_mxKur : ursubmx A === Aur.
proof: Proof. by move=> i j; rewrite /A /block_mx /ursubmx /lcutmx /rcutmx /trmx; rewrite -> pastemxEl, pastemxEr; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms