proposition: Lemma Zp_mulz1 : right_id Zp1 Zp_mul.
proof: Proof. by move=> x; rewrite Zp_mulC 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)