proposition: Lemma sig_tilt (z: 'S_k) (i j: 'I_k) : i != j -> ~~ odd_perm (tilt i j z) = odd_perm z.
proof: Proof. by move => hij; rewrite odd_mul_tperm hij negbK /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor