proposition: Lemma Zp_mulzV x : coprime p x -> Zp_mul x (Zp_inv x) = Zp1.
proof: Proof. by move=> Ux; rewrite /= Zp_mulC Zp_mulVz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)