proposition: Lemma cardG_gt1 : (#|G| > 1) = (G :!=: 1).
proof: Proof. by rewrite trivg_card_le1 ltnNge. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)