proposition: Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f -> perm_eq (index_enum T) [seq f i | i <- index_enum T].
proof: Proof. rewrite /index_enum; case: index_enum_key => /= fbij. rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. case: fbij => g fg gf. rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _ (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))). by rewrite size_filter enumP. by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist