. intro hval
  simp [int_val, nat_valuation] at hval
  cases abs_a : (natAbs a) with
  | zero => exact natAbs_eq_zero.1 abs_a
  | succ n =>
    cases hp : p with
    | zero =>
      rw [hp] at gt1
      apply False.elim ((of_decide_eq_true rfl : ¬1 < 0) gt1)
    | succ p' =>
      cases hp' : p' with
      | zero =>
        rw [hp, hp'] at gt1
        apply False.elim ((of_decide_eq_true rfl : ¬1 < 1) gt1)
      | succ n =>
        simp [hp, hp', abs_a, nat_valuation_aux, nat_valuation_aux'] at hval
case mp
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ int_val p a = ⊤ → a = 0

case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤
case mpr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
a : ℤ
⊢ a = 0 → int_val p a = ⊤