proposition: Lemma unitZpE x : p > 1 -> ((x%:R : 'Z_p) \is a GRing.unit) = coprime p x.
proof: Proof. move=> p_gt1; rewrite qualifE /=. by rewrite val_Zp_nat ?Zp_cast ?coprime_modr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)