proposition: Lemma porbit_setP s t x : porbit s x =i porbit t x <-> porbit s x = porbit t x.
proof: Proof. by rewrite porbit.unlock; exact: setP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)