Theorem: nat_val_succ (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
⊢ nat_valuation (q + 2) (m + 1) = if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation (q + 2) ((m + 1) / (q + 2)) + 1
Tactic:
simp [nat_valuation_add_two, nat_val_aux_succ]
State after:
no goals