proposition: Lemma cycle_decE s : \prod_(C in cycle_dec s) C = s.
proof: Proof. Proof using. have /and3P[/eqP Hcov Htriv _] := partition_psupport s. apply perm_decE => //; first by rewrite Hcov. apply/astabP => C /porbit_set_astabs. rewrite -astab1_set => /astabP; apply. by rewrite inE. 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