proposition: Lemma sign_tilt2 (z: 'S_k) (i j: 'I_k) : i != j -> (-1)^+(tilt i j z) = -1* ((-1) ^+ z) :>R.
proof: Proof. move => hij. rewrite odd_mul_tperm hij /= mulNr mul1r. by case: (odd_perm z); rewrite /= expr0 expr1 ?opprK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor