proposition: Lemma from_good_to_perm (g: {ffun 'I_k -> 'I_l}) (P : {ffun 'I_k -> 'I_l} -> R) : injective g -> \sum_(f | good g f) P f = \sum_(phi : 'S_k) (P (finfun (g \o phi))).
proof: Proof. move => hg. rewrite (reindex_onto (fun p:'S_k => finfun (g \o p)) (perm_f g)) /=. - apply/eq_big => // p. have hinj : injective (finfun (g \o p)). + have htemp : injective (g \o p) by apply: inj_comp => //; apply: perm_inj. move => x y; rewrite !ffunE => heq. exact: htemp. have hcodom : forall x, (x \in codom (finfun (g \o p))) = (x \in codom g) by move => x; rewrite codom_perm. apply/andP; split. + apply/andP; split; first exact/injectiveP. apply/forallP => x; by rewrite hcodom. apply/eqP/permP => x. have := perm_fE hinj hcodom x. by rewrite ffunE => /hg ->. move => /= f. case/goodP => h1 h2. apply/ffunP => /= x. by rewrite ffunE (perm_fE h1 h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor