proposition: Lemma order_cyclic t : t \is cyclic -> #[t] = #|psupport t|.
proof: Proof. Proof using. rewrite /order => Hcy. rewrite (cycle_cyclic Hcy) card_imset ?card_ord //. move: Hcy => /cyclicP[x Hx Hsupp]. move=> [i Hi] [j Hj] /= /(congr1 (fun s => s x)) Hij. apply val_inj => /=; apply/eqP. rewrite -(nth_uniq x _ _ (uniq_traject_porbit t x)) ?size_traject -?Hsupp //. by rewrite !nth_traject // -!permX Hij. 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