proposition: Lemma Zp_group_set : group_set Zp.
proof: Proof. by rewrite /Zp; case: (p > 1); apply: groupP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)