rw [if_neg hmq]
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) = 0