proposition: Lemma disjoint_cycle_dec s : disjoint_psupports (cycle_dec s).
proof: Proof. Proof using. apply: disjoint_perm_dec. by have /and3P[] := partition_psupport s. 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