proposition: Lemma Sym_trans : [transitive^n 'Sym_T, on setT | 'P].
proof: Proof. apply/imsetP; pose t1 := [tuple of enum T]. have dt1: t1 \in n.-dtuple(setT) by rewrite inE enum_uniq; apply/subsetP. exists t1 => //; apply/setP=> t; apply/idP/imsetP=> [|[a _ ->{t}]]; last first. by apply: n_act_dtuple => //; apply/astabsP=> x; rewrite !inE. case/dtuple_onP=> injt _; have injf := inj_comp injt enum_rank_inj. exists (perm injf); first by rewrite inE. apply: eq_from_tnth => i; rewrite tnth_map /= [aperm _ _]permE; congr tnth. by rewrite (tnth_nth (enum_default i)) enum_valK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)