proposition: Lemma classG_eq1 x : (x ^: G == 1) = (x == 1).
proof: Proof. apply/eqP/eqP=> [xG1 | ->]; last exact: class1G. by have:= class_refl x; rewrite xG1 => /set1P. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)