cases LE.le.lt_or_eq m_le_sM with
| inl mltsM =>
  exact IH m (Nat.le_of_lt_succ mltsM) hm n hmq
| inr meqsM =>
  cases em ((m / q) % q == 0) with
  | inl h =>
    rw [nat_valuation_aux'', nat_valuation_aux'', dif_pos h]
    simp only [beq_iff_eq, Nat.cast_succ]
    rw [dif_pos hmq]
    simp only [meqsM]
    rw [meqsM] at hm h hmq
    exact IH (M.succ/q) (Nat.le_of_lt_succ (Nat.div_lt_self hm hq))
      (Nat.div_pos_of_mod hm hq hmq) (n+1) (by simpa using h)
  | inr h =>
    rw [nat_valuation_aux'', nat_valuation_aux'', dif_neg h, dif_pos, nat_valuation_aux'', dif_neg h]
    simp
    . simp only [hmq]
case succ
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
no goals