proposition: Lemma cutmxK : forall A, pastemx (lcutmx A) (rcutmx A) === A.
proof: Proof. move=> A i j. rewrite/pastemx/lcutmx/rcutmx. case: splitP; case=> /= k kprf eqk. by have <- : j = lshift n2 (Ordinal kprf); [apply ord_inj; apply eqk | reflexivity]. by have <- : j = rshift n1 (Ordinal kprf); [apply ord_inj; apply eqk | reflexivity]. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms