Theorem: nat_valuation_aux'_of_dvd (ECTate/Algebra/ValuedRing.lean)

State before:
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
Tactic:
simp [nat_valuation_aux', nat_valuation_aux''_of_dvd q hq m hm 0 hmq]
State after:
no goals