proposition: Lemma val_Fp_nat n : (n%:R : 'F_p) = (n %% p)%N :> nat.
proof: Proof. by rewrite Zp_nat /= 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)