simpa [is_local_singular_point, weierstrass] using h.1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
h : is_local_singular_point evr.valtn e (0, 0)
⊢ 0 < SurjVal.v evr.valtn e.a6
no goals