exact nat_valuation_aux'_of_not_dvd _ _ _ _ h
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) = 0
no goals