simp [nat_valuation_aux', nat_valuation_aux''_of_dvd q hq m hm 0 hmq]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q = 0
⊢ nat_valuation_aux' q hq m hm = nat_valuation_aux' q hq (m / q) (_ : 0 < m / q) + 1
no goals