proposition: Lemma porbitPmin s x y : y \in porbit s x -> exists2 i, i < #[s] & y = (s ^+ i) x.
proof: Proof. by rewrite porbit.unlock=> /imsetP [z /cyclePmin[ i Hi ->{z}] ->{y}]; 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)