proposition: Lemma unit_Zp_expg (u : {unit 'I_p}) n : val (u ^+ n) = inZp (val u ^ n) :> 'I_p.
proof: Proof. apply: val_inj => /=; elim: n => [|n IHn] //. by rewrite expgS /= IHn expnS modnMmr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)