proposition: Lemma col'Kr m n1 n2 j2 (A1 : 'M_(m, n1)) (A2 : 'M_(m, n2)) : col' (rshift n1 j2) (@row_mx m n1 n2 A1 A2) = castmx (erefl m, mx'_cast n1 j2) (row_mx A1 (col' j2 A2)).
proof: Proof. apply/matrixP=> i j; symmetry; rewrite castmxE mxE cast_ord_id. case: splitP => j' /= def_j. rewrite mxE -(row_mxEl _ A2); congr (row_mx _ _ _); apply: ord_inj. by rewrite /= def_j /bump leqNgt ltn_addr. rewrite 2!mxE -(row_mxEr A1); congr (row_mx _ _ _ _); apply: ord_inj. by rewrite /= def_j /bump leq_add2l addnCA. 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)