intro m mle0 hm n hmq
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
⊢ ∀ (m : ℕ),
    m ≤ Nat.zero →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m ≤ Nat.zero
hm : 0 < m
n : ℕ
hmq : m % q = 0
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1