proposition: Lemma perm_eq_permuted_tuple (s : seq T) (H : size s == n) : forall s1, perm_eq s s1 -> s1 \in [seq tval t | t <- permuted_tuple (Tuple H)].
proof: Proof. Proof using. set t := Tuple H; have Ht : perm_eq s t by []. move=> s1 Hss1; rewrite perm_sym in Hss1. have:= perm_trans Hss1 Ht => /tuple_permP[p Hs1]. apply/mapP; set t1 := (X in _ = tval X) in Hs1; exists t1; last exact Hs1. rewrite /permuted_tuple; apply/mapP. by exists p; first by rewrite mem_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles