proposition: Lemma reindex_with_tilt (P: 'S_k -> R) (i j: 'I_k) : i != j -> \sum_(z : 'S_k) (P z) = \sum_(z: 'S_k | odd_perm z) (P z + P (tilt i j z)).
proof: Proof. move => hij. rewrite (bigID (fun z:'S_k => odd_perm z)) big_split /=; congr (_ + _). pose C := fun z => ~~ odd_perm z. pose D := fun z => odd_perm z. pose D' := fun z => C _ (tilt i j z). have hD : D _ =1 D' by move=> p; rewrite /D /D' /C sig_tilt. by rewrite (eq_bigl _ _ hD) /D' -(reindex_inj (@tilt_inj i j)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor