proposition: Theorem cycle_decP s : unique (cycle_dec_spec s) (cycle_dec s).
proof: Proof. Proof using. split; first by constructor; [ exact: cyclic_dec | exact: disjoint_cycle_dec | exact: cycle_decE]. move=> A [Hcy Hdisj Hprod]. apply/setP => /= C; apply/imsetP/idP => /= [| HC]. - rewrite -{1}Hprod => [[X HX1] ->]. have [/= x Hx] := disjoint_psupports_porbits Hcy Hdisj HX1. rewrite -{1}(psupport_restr_perm HX1). move=> /(disjoint_psupports_of_decomp Hdisj (disjoint_cycle_dec s)). rewrite Hprod cycle_decE => /(_ erefl Hx) <- //. by apply/imsetP; exists X; rewrite -Hprod. - have:= HC => /disjoint_psupports_cycles /= /(_ Hcy Hdisj) /imsetP[x _]. rewrite Hprod => Hsupp. have Hx: porbit s x \in porbit_set s. rewrite inE; apply/andP; split. + by apply/imsetP; exists x. + by rewrite -Hsupp; rewrite card_psupport_noteq1. exists (porbit s x) => //. have:= disjoint_psupports_of_decomp Hdisj (disjoint_cycle_dec s). rewrite Hprod cycle_decE => /(_ erefl C (restr_perm (porbit s x) s) HC). apply; last by rewrite psupport_restr_perm. by apply/imsetP; exists (porbit s x). 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