proposition: Lemma commute_cyclic c t : c \is cyclic -> t \in 'C[c] -> perm_on (psupport c) t -> exists i, t = c ^+ i.
proof: Proof. Proof using. move=> /cyclicP[x Hx Hsupp] Hcent1 Hon. have /= := cent1_act_porbit x Hcent1. have:= Hx; rewrite -(perm_closed _ Hon). move: Hon; rewrite Hsupp -eq_porbit_mem => Hon /eqP -> cx_stable. move: Hcent1 => /cent1P Hcomm. have /= := mem_setact ('P) t (porbit_id c x). rewrite cx_stable => /porbitP[i]; rewrite apermE => Hi. exists i; apply/permP => z. have [/porbitP[j ->{z}]|] := (boolP (z \in (porbit c x))). - by rewrite -!permM -(commuteX j Hcomm) -expgD addnC expgD !permM Hi. - move=> Hz; move: Hon => /subsetP/(_ z)/contra/(_ Hz). rewrite inE negbK => /eqP ->. by move: Hz; rewrite -Hsupp in_psupport negbK => /eqP /permX_fix ->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype