proposition: Lemma char_Fp : p \in [char 'F_p].
proof: Proof. by rewrite !inE -Fp_nat_mod p_pr ?modnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool choice eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup) mathcomp(ssralg finalg countalg)