fact: Definition char (R : semiRingType) : nat_pred := [pred p | prime p & p%:R == 0 :> R].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)