proposition: Lemma card_Fp : #|'F_p| = p.
proof: Proof. by rewrite card_ord Fp_cast. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)