proposition: Lemma natf0_char n : n > 0 -> n%:R == 0 :> R -> exists p, p \in char R.
proof: Proof. move=> n_gt0 nR_0; exists (pdiv n`_(char R)). apply: pnatP (pdiv_dvd _); rewrite ?part_pnat // ?pdiv_prime //. by rewrite ltn_neqAle eq_sym partn_eq1 // -natf_neq0 nR_0 /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)