proposition: Lemma cyclic_dec s : {in (cycle_dec s), forall C, C \is cyclic}.
proof: Proof. Proof using. move => C /imsetP[X HX ->]. by rewrite unfold_in porbit_set_restr ?cards1. 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