rw [decr_val_p]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ decr_val_p p k = k
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ (if (k % ↑p == 0) = true then k / ↑p else k) = k