proposition: Lemma porbit_id s x : x \in porbit s x.
proof: Proof. by rewrite -{1}[x]perm1 (mem_porbit s 0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)