proposition: Lemma card_Zp : p > 0 -> #|Zp| = p.
proof: Proof. rewrite /Zp; case: p => [|[|p']] //= _; first by rewrite cards1. by rewrite cardsT card_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)