proposition: Lemma Zp1_expgz x : Zp1 ^+ x = x.
proof: Proof. by rewrite Zp_expg; apply: Zp_mul1z. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)