proposition: Lemma in_one_group x : (x \in 1%G) = (x == 1).
proof: Proof. by rewrite -[x \in _]/(x \in [set 1]) !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)