proposition: Lemma mx_col_rshift : forall m n1 n2 j2 A1 (A2 : 'M_(m, n2)), mx_col (rshift n1 j2) (pastemx A1 A2) === mx_col j2 A2.
proof: Proof. by rewrite/mx_col=> m n1 n2 j1 A1 A2 i j; 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