proposition: Lemma col_perm_inj n (s : 'S_n) T m : injective (@col_perm T m n s).
proof: Proof. move=> x y; rewrite /col_perm => /matrixP xy; apply/matrixP => i j. by move: (xy i (s^-1%g j)); rewrite !mxE permKV. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2