rw [nat_valuation_aux'', dif_neg hmq_bool]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
hmq_bool : ¬(m % q == 0) = true
⊢ nat_valuation_aux'' q hq m hm 0 = 0
no goals