proposition: Lemma trivgPn : reflect (exists2 x, x \in G & x != 1) (G :!=: 1).
proof: Proof. rewrite -subG1. by apply: (iffP subsetPn) => [] [x Gx x1]; exists x; rewrite ?inE in x1 *. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)