simp
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (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
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true

case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (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
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true

case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (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
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (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
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ m % q = 0