proposition: Lemma ntransitive_primitive m : 1 < m -> [transitive^m G, on S | to] -> [primitive G, on S | to].
proof: Proof. move=> lt1m /(ntransitive_weak lt1m) {m lt1m}tr2G. have trG: [transitive G, on S | to] by apply: ntransitive1 tr2G. have [x Sx _]:= imsetP trG; rewrite (trans_prim_astab Sx trG). apply/maximal_eqP; split=> [|H]; first exact: subsetIl; rewrite subEproper. case/predU1P; first by [left]; case/andP=> sCH /subsetPn[a Ha nCa] sHG. right; rewrite -(subgroup_transitiveP Sx sHG trG _) ?mulSGid //. have actH := subset_trans sHG (atrans_acts trG). pose y := to x a; have Sy: y \in S by rewrite (actsP actH). have{nCa} yx: y != x by rewrite inE (sameP astab1P eqP) (subsetP sHG) in nCa. apply/imsetP; exists y => //; apply/eqP. rewrite eqEsubset acts_sub_orbit // Sy andbT; apply/subsetP=> z Sz. have [-> | zx] := eqVneq z x; first by rewrite orbit_sym mem_orbit. pose ty := [tuple y; x]; pose tz := [tuple z; x]. have [Sty Stz]: ty \in 2.-dtuple(S) /\ tz \in 2.-dtuple(S). by rewrite !inE !memtE !subset_all /= !mem_seq1 !andbT; split; apply/and3P. case: (atransP2 tr2G Sty Stz) => b Gb [->] /esym/astab1P cxb. by rewrite mem_orbit // (subsetP sCH) // inE Gb. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)