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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
⊢ nat_valuation_aux p hp 0 = ⊤
Tactic:
simp [nat_valuation_aux]
State after:
no goals