proposition: Lemma mx_row'_paste : forall m n1 n2 i0 (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)), mx_row' i0 (pastemx A1 A2) === pastemx (mx_row' i0 A1) (mx_row' i0 A2).
proof: Proof. by reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms