simp [nat_valuation_aux''_of_not_dvd q hq m hm hmq]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ (match m, hm with
    | m, hm => ↑(nat_valuation_aux'' q hq m hm 0)) =
    0
no goals