proposition: Lemma charf_eq : char R =i (p : nat_pred).
proof: Proof. move=> q; apply/andP/eqP=> [[q_pr q0] | ->]; last by rewrite charf0. by apply/eqP; rewrite eq_sym -dvdn_prime2 // dvdn_charf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)