proposition: Lemma dvdn_charf n : (p %| n)%N = (n%:R == 0 :> R).
proof: Proof. apply/idP/eqP=> [/dvdnP[n' ->]|n0]; first by rewrite natrM charf0 mulr0. apply/idPn; rewrite -prime_coprime // => /eqnP pn1. have [a _ /dvdnP[b]] := Bezoutl n (prime_gt0 charf_prime). move/(congr1 (fun m => m%:R : R))/eqP. by rewrite natrD !natrM charf0 n0 !mulr0 pn1 addr0 oner_eq0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)