proposition: Lemma porbit_sym s x y : (x \in porbit s y) = (y \in porbit s x).
proof: Proof. by rewrite -!eq_porbit_mem eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)