proposition: Lemma dvdz_charf (R : ringType) (p : nat) : p \in [char R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R).
proof: Proof. move=> charRp [] n; rewrite [LHS](dvdn_charf charRp)//. by rewrite NegzE abszN rmorphN// oppr_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)