Theorem: Int.primeVal_pos_iff (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
⊢ 0 < SurjVal.v (primeVal hp) k ↔ ↑p ∣ k
Tactic:
simp [← not_iff_not]
State after:
no goals