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=>/=. move=>fbij. rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. inversion fbij. 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. move=> x _ /=. apply/eqP/eqP. by move=>/(f_equal g) <-. by move=>->. Qed.
imports: Reals mathcomp(all_ssreflect all_algebra vector reals classical_sets Rstruct) infotheo(convex)