proposition: Lemma Alt_trans : [transitive^n.-2 'Alt_T, on setT | 'P].
proof: Proof. case n_m2: n Sym_trans => [|[|m]] /= tr_m2; try exact: ntransitive0. have tr_m := ntransitive_weak (leqW (leqnSn m)) tr_m2. case/imsetP: tr_m2; case/tupleP=> x; case/tupleP=> y t. rewrite !dtuple_on_add 2![x \in _]inE inE negb_or /= -!andbA. case/and4P=> nxy ntx nty dt _; apply/imsetP; exists t => //; apply/setP=> u. apply/idP/imsetP=> [|[a _ ->{u}]]; last first. by apply: n_act_dtuple => //; apply/astabsP=> z; rewrite !inE. case/(atransP2 tr_m dt)=> /= a _ ->{u}. case odd_a: (odd_perm a); last by exists a => //; rewrite !inE /= odd_a. exists (tperm x y * a); first by rewrite !inE /= odd_permM odd_tperm nxy odd_a. apply/val_inj/eq_in_map => z tz; rewrite actM /= /aperm; congr (a _). by case: tpermP ntx nty => // <-; rewrite tz. 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)