proposition: Lemma fz_tilt_0 (i j: 'I_k) (f: {ffun 'I_k -> 'I_l}) z: i != j -> f i = f j -> weight f z + weight f (tilt i j z) = 0.
proof: Proof. rewrite /weight => hij hf. rewrite sign_tilt2 // !mulNr mul1r -mulrBr. set b1 := \big[*%R/1]_( _ < _ ) _. set b2 := \big[*%R/1]_( _ < _ ) _. suff -> : b1 = b2 by rewrite subrr mulr0. rewrite /b1 {b1} /b2 {b2} (bigD1 j) //= (bigD1 i) //=. rewrite [RHS](bigD1 j) //= [X in _ = _ * X](bigD1 i) //=. rewrite !permM tpermR tpermL hf !mulrA. congr (_ * _). by rewrite -!mulrA; congr (_ * _); rewrite mulrC -mulrA mulrCA. by apply/eq_big => // x /andP [h1 h2]; rewrite permM tpermD // eq_sym. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor