proposition: Lemma char_Fp_0 : p%:R = 0 :> 'F_p.
proof: Proof. exact: GRing.charf0 char_Fp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)