proposition: Lemma porbit_perm s i x : porbit s ((s ^+ i) x) = porbit s x.
proof: Proof. by apply/eqP; rewrite eq_porbit_mem mem_porbit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)