rw [Nat.le_zero] at mle0
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
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m = 0
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