proposition: Lemma eq_porbit_mem s x y : (porbit s x == porbit s y) = (x \in porbit s y).
proof: Proof. apply/eqP/idP; first by move<-; exact: porbit_id. rewrite porbit.unlock => /imsetP[si s_si ->]. apply/setP => z; apply/imsetP/imsetP=> [] [sj s_sj ->]. by exists (si * sj); rewrite ?groupM /aperm ?permM. exists (si^-1 * sj); first by rewrite groupM ?groupV. by rewrite /aperm permM permK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)