proposition: Lemma submxK : block_mx ulsubmx ursubmx llsubmx lrsubmx === A.
proof: Proof. rewrite/block_mx/ulsubmx/ursubmx/llsubmx/lrsubmx. rewrite -> !cutmxK => i j. rewrite/rcutmx/lcutmx/pastemx/trmx. case: splitP => i' eqii'. by have -> : lshift m2 i' = i; [apply ord_inj|reflexivity]. by have -> : rshift m1 i' = i; [apply ord_inj|reflexivity]. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms