proposition: Lemma Fp_fieldMixin : GRing.ComUnitRing_isField 'F_p.
proof: Proof. constructor => x nzx. rewrite qualifE /= prime_coprime ?gtnNdvd ?lt0n //. case: (ltnP 1 p) => [lt1p | ]; last by case: p => [|[|p']]. by rewrite Zp_cast ?prime_gt1 ?pdiv_prime. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)