proposition: Lemma cycle_cyclic t : t \is cyclic -> cycle t = [set t ^+ i | i : 'I_#|psupport t|].
proof: Proof. Proof using. move/cyclicP => [x Hx Hsupp]; rewrite Hsupp. apply/setP => C; apply/cycleP/imsetP => [[i -> {C}] | [i Hi -> {C}]]. - have /(ltn_pmod i) Hmod : 0 < #|porbit t x|. by rewrite card_gt0; apply/set0Pn; exists x. exists (Ordinal Hmod) => //=; apply/permP => y /=. case: (boolP (y \in porbit t x)). + by rewrite -eq_porbit_mem => /eqP <-; exact: porbit_mod. + rewrite -Hsupp in_psupport negbK => /eqP Ht. by rewrite !permX_fix. - by exists i. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action ssralg) tools permcomp