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 : ℤ
hval :
  (match p, natAbs a with
    | x, 0 => ⊤
    | 0, Nat.succ n => 0
    | 1, Nat.succ x => ⊤
    | Nat.succ (Nat.succ q), Nat.succ m => nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (m + 1)) =
    ⊤
⊢ a = 0
no goals