simp only [natAbs_cast, int_val]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ int_val p ↑p = 1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1