proposition: Lemma porbits_perm_of_setpart P : partition P [set: T] -> porbits (perm_of_setpart P) = P.
proof: Proof. Proof using. move=> Hpart; apply /setP => X. apply /idP/idP => HX. - case: (boolP (X \in porbit_set (perm_of_setpart P))). + rewrite porbit_set_of_disjoint; last exact: disj_perm_of_setpart. move => /bigcupP[C] /imsetP[X0]. rewrite inE => /andP[H HX0] ->. by rewrite porbit_set_of_set // inE => /eqP ->. + rewrite inE => /nandP[]; first by rewrite HX. move: HX => /imsetP[x _ ->{X}]. rewrite psupport_card_porbit => Hsupp. have:= Hsupp; rewrite in_psupport negbK porbit_fix => /eqP ->. move: Hsupp; rewrite psupport_of_disjoint; last exact: disj_perm_of_setpart. rewrite -(big_imset id) /=; first last. move=> C D /imsetP[c]; rewrite inE => /andP[_ cardc ->{C}]. move=> /imsetP[d]; rewrite inE => /andP[_ cardd ->{D}]. by rewrite !psupport_perm_of_porbit // => ->. rewrite -imset_comp psupports_perm_of_porbit => /bigcupP. move=> /exists_inP; rewrite -[X in (is_true X) -> _]negbK. have xinP : x \in cover P by rewrite (cover_partition Hpart). have:= xinP; rewrite -mem_pblock => xPblock. rewrite negb_exists_in => /forall_inP/(_ (pblock P x))/contraL/(_ xPblock). rewrite inE => /nandP[]; first by rewrite pblock_mem. rewrite -leqNgt leq_eqVlt => /orP[/cards1P[y Hy]|]. * move: xPblock; rewrite Hy inE => /eqP ->. by rewrite -Hy; apply pblock_mem. * rewrite ltnS leqn0 cards_eq0 => /eqP H. by move: xPblock; rewrite H inE. - case: (boolP (#|X| == 1)). + move => /cards1P[x Hx]; subst X. apply /imsetP; exists x => //. apply esym; apply/eqP; rewrite -porbit_fix. rewrite -[_ == x]negbK -in_psupport psupport_of_disjoint; last exact: disj_perm_of_setpart. apply /bigcupP => /exists_inP; apply /negP; rewrite negb_exists_in. apply /forall_inP => C /imsetP[x0]; rewrite inE => /andP[Hx0 Hcard] ->. rewrite psupport_perm_of_porbit //. move: Hpart => /and3P[_ /trivIsetP /(_ [set x] x0) Hxx0 _]. move: Hxx0 => /(_ HX Hx0) Htmp. have /eqP {}/Htmp : [set x] <> x0 by move => Heq; move: Hcard; rewrite -Heq cards1. rewrite -setI_eq0 => /eqP Hxx0. apply /negP => Hx. suff: x \in set0 by rewrite inE. by rewrite -Hxx0 inE Hx andbT inE. + have:= Hpart => /and3P[_ _ Hset0]. move=> H; move: H HX Hset0. rewrite neq_ltn => /orP[ | Hcard HX Hset0]. by rewrite ltnS leqn0 cards_eq0 => /eqP -> ->. suff: X \in porbit_set (perm_of_setpart P) by rewrite inE => /andP[]. rewrite porbit_set_of_disjoint; last exact: disj_perm_of_setpart. apply /bigcupP; exists (perm_of_porbit X); last by rewrite porbit_set_of_set ?inE. apply /imsetP; exists X => //. by rewrite inE; apply /andP; split. 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