proposition: Lemma charf'_nat n : (char R)^'.-nat n = (n%:R != 0 :> R).
proof: Proof. have [-> | n_gt0] := posnP n; first by rewrite eqxx. apply/idP/idP => [|nz_n]; last first. by apply/pnatP=> // p p_pr p_dvd_n; apply: contra nz_n => /dvdn_charf <-. apply: contraL => n0; have [// | p charRp] := natf0_char _ n0. have [p_pr _] := andP charRp; rewrite (eq_pnat _ (eq_negn (charf_eq charRp))). by rewrite p'natE // (dvdn_charf charRp) n0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)