proposition: Lemma charf0P : char R =i pred0 <-> (forall n, (n%:R == 0 :> R) = (n == 0)%N).
proof: Proof. split=> charF0 n; last by rewrite !inE charF0 andbC; case: eqP => // ->. have [-> | n_gt0] := posnP; first exact: eqxx. by apply/negP; case/natf0_char=> // p; rewrite charF0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)