proposition: Lemma mx_col'_lshift : forall m n1 n2 j1 (A1 : 'M_(m, n1.+1)) A2, mx_col' (lshift n2 j1) (pastemx A1 A2) === pastemx (mx_col' j1 A1) A2.
proof: Proof. move=> m n1 n2 j1 A1 A2 i /= j. case: (splitP j) => j' def_j'. have -> : j = lshift n2 j' by apply ord_inj; apply def_j'. rewrite -> pastemxEl; rewrite /mx_col'. have -> : lift (lshift n2 j1) (lshift n2 j') = lshift n2 (lift j1 j'); last by rewrite -> pastemxEl; reflexivity. by apply ord_inj. have -> : j = rshift n1 j' by apply ord_inj; apply def_j'. rewrite -> pastemxEr; rewrite /mx_col'. have -> : lift (lshift n2 j1) (rshift n1 j') = (rshift n1.+1 j'); last by rewrite -> pastemxEr; reflexivity. apply ord_inj => /=. rewrite/bump //= addSnnS addnS -def_j' -(addn1 j) addnC. have -> : j1 <= j=>//. rewrite def_j' {def_j'}. by apply leq_trans with n1; [apply j1 | apply leq_addr]. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms