proposition: Lemma perm_of_porbitE C x : x \in C -> C = porbit (perm_of_porbit C) (head x (enum C)).
proof: Proof. Proof using. rewrite -mem_enum; have:= erefl (enum C). case: {2 3 4}(enum C) => [|a l HC _ /=]; first by rewrite in_nil. apply /setP => y; apply /idP/porbitP => [| [n ->]]. - rewrite -mem_enum => Hy; exists (index y (enum C)). elim: (index y _) {1 2 4}y Hy (erefl (index y (enum C))) => [| m IHm] {}y Hy Hind. have:= nth_index y Hy; rewrite Hind HC /= => <-. by rewrite expg0 perm1. have Hm : m < size (enum C). by move: Hy; rewrite -index_mem Hind; apply leq_trans. have Hnth : index (nth y (enum C) m) (enum C) = m. by rewrite index_uniq // enum_uniq. have Hnthin : (nth y (enum C) m) \in enum C. by rewrite -index_mem Hnth. rewrite expgSr permM -(IHm (nth y (enum C) m)) //. rewrite permE next_nth Hnthin {1}HC Hnth. have /negbTE Hya : y != a. by apply /eqP => Heq; move: Hind; rewrite Heq HC index_head. move: Hind; rewrite HC -cat1s index_cat. rewrite inE Hya /= add1n => [[]] <-. rewrite nth_index //. by move: Hy; rewrite HC inE Hya. - elim: n => [|m IHm]. + by rewrite expg0 perm1 -mem_enum HC mem_head. + by rewrite expgSr permM permE -mem_enum mem_next mem_enum. 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