proposition: Lemma cyclicP c : reflect (exists2 x, x \in psupport c & psupport c = porbit c x) (c \is cyclic).
proof: Proof. Proof using. apply (iffP cards1P) => [[sc Hsc] | [x Hx Hsc]]. - have:= partition_psupport c; rewrite Hsc => /cover_partition. rewrite /cover big_set1 => Hsupp; subst sc. have : psupport c != set0. rewrite -psupport_eq0 porbit_set_eq0 Hsc. apply/negP => /eqP Habs. by have:= set11 (psupport c); rewrite Habs in_set0. move=> /set0Pn[x Hx]; exists x; first by []. have : porbit c x \in porbit_set c. by rewrite inE imset_f //= psupport_card_porbit. by rewrite Hsc in_set1 => /eqP ->. - exists (porbit c x); apply triv_part. + by rewrite inE imset_f //= psupport_card_porbit. + by rewrite -Hsc; apply: partition_psupport. 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