proposition: Lemma pastemxKr : forall A1 A2, rcutmx (pastemx A1 A2) === A2.
proof: Proof. by move=> A1 A2 i j; rewrite /rcutmx; rewrite -> pastemxEr; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms