proposition: Lemma psupport_perm_of_porbit C : #|C| > 1 -> psupport (perm_of_porbit C) = C.
proof: Proof. Proof using. move=> Hsize; apply /setP => x. rewrite in_psupport permE. apply/idP/idP => [|Hx]; rewrite next_nth. - by apply contraR; rewrite -mem_enum => /negbTE ->. - rewrite mem_enum Hx. move: Hsize Hx; rewrite -mem_enum cardE. case: (enum C) (enum_uniq (pred_of_set C)) => // a [// | b l] /=. move=> /and3P[]; rewrite inE => /norP[/negbTE Hab Ha] Hb Huniq _. rewrite !inE => /orP[/eqP -> | /orP[/eqP -> |Hx]]. + by rewrite eq_refl /= eq_sym Hab. + rewrite Hab eq_refl /=. case: {2 3}l (erefl l) => [|c l0 Hl]; first by rewrite Hab. by apply /eqP => Heq; move: Hb; rewrite -Heq Hl mem_head. + have /negbTE Hbx: (b != x). by apply /eqP => Heq; move: Hb; rewrite Heq Hx. have /negbTE Hax: (a != x). by apply /eqP => Heq; move: Ha; rewrite Heq Hx. have Hxb: x \in (b :: l) by rewrite inE Hx orbT. rewrite Hax Hbx. case (ltnP (index x l).+2 (size (b :: l))) => Hindex. * have:= Hxb; rewrite -index_mem => Hindex1. rewrite -{2}(nth_index a Hxb) nth_uniq //=; last by apply /andP. by rewrite Hbx gtn_eqF. * by rewrite nth_default ?Hax. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles