proposition: Lemma porbitP s x y : reflect (exists i, y = (s ^+ i) x) (y \in porbit s x).
proof: Proof. apply (iffP idP) => [/porbitPmin [i _ ->]| [i ->]]; last exact: mem_porbit. by exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)