proposition: Lemma tuple_exist_perm_sort (T : eqType) n (r : rel T) (t : n.-tuple T) : exists s : 'S_n, t = perm_tuple s (sort_tuple r t).
proof: Proof. rewrite /perm_tuple. have : perm_eq t (sort_tuple r t) by rewrite perm_sym perm_sort perm_refl. case/tuple_permP => u Hu; exists u. case: t Hu => t /= Ht Hu. apply eq_from_tnth => i /=. rewrite /tnth /= -Hu. apply: set_nth_default. move/eqP : {Hu}Ht => ->; by case: i. Qed.
imports: mathcomp(all_ssreflect fingroup perm)