proposition: Lemma mx_col_lshift : forall m n1 n2 j1 (A1 : 'M_(m, n1)) A2, mx_col (lshift n2 j1) (pastemx A1 A2) === mx_col j1 A1.
proof: Proof. by rewrite/mx_col=> m n1 n2 j1 A1 A2 i j; rewrite -> pastemxEl; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms