proposition: Lemma Zp_abelian : abelian [set: 'I_p].
proof: Proof. exact: FinRing.zmod_abelian. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)