proposition: Lemma sum_bad : \sum_(fz : Z | ~~ injectiveb fz.1) (weight fz.1 fz.2) = 0.
proof: Proof. rewrite (split_sumZ_fs _ (fun x => ~~ injectiveb x)). apply/big1 => f /injectivePn [x [y hxy hf]] /=. rewrite (reindex_with_tilt _ hxy). by apply/big1 => s _; rewrite fz_tilt_0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor