proposition: Lemma porbitV s : porbit s^-1 =1 porbit s.
proof: Proof. move=> x; apply/setP => y; rewrite porbit_sym. by apply/porbitP/porbitP => -[i ->]; exists i; rewrite expgVn ?permK ?permKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)