proposition: Lemma proper1G : ([1] \proper G) = (G :!=: 1).
proof: Proof. by rewrite properEneq sub1G andbT eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)