proposition: Lemma porbits_tperm x y : porbits (tperm x y) = [set x; y] |: [set [set z] | z : T & (x != z) && (y != z)].
proof: Proof. rewrite /porbits; apply/setP => S; rewrite !inE. apply/imsetP/idP => [[z _ ->{S}] | /orP[/eqP->{S} | /imsetP[z]]]. - case: (x =P z) => [<-{z} | /eqP xz]; first by rewrite porbit_tpermL eqxx. case: (y =P z) => [{xz} <-{z} | /eqP yz]; first by rewrite porbit_tpermR eqxx. rewrite porbit_tpermD //; apply/orP; right. by apply/imsetP; exists z => //; rewrite inE xz yz. - by exists x => //; rewrite porbit_tpermL. - rewrite inE => /andP[xz yz] ->{S}. by exists z => //; rewrite porbit_tpermD. 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