proposition: Lemma col'Kl m n1 n2 j1 (A1 : 'M_(m, n1.+1)) (A2 : 'M_(m, n2)) : col' (lshift n2 j1) (row_mx A1 A2) = row_mx (col' j1 A1) A2.
proof: Proof. apply/matrixP=> i /= j; symmetry; rewrite 2!mxE; case: split_ordP => j' ->. by rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj. rewrite -(row_mxEr A1); congr (row_mx _ _ _); apply: ord_inj => /=. by rewrite /bump -ltnS -addSn ltn_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)