simp only [val_discr_to_nat, coe_toNat_eq_self, ne_eq, v_eq_top_iff_zero]
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ↑(val_discr_to_nat valp e) = v valp (Model.discr e.toModel)
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
⊢ ¬Model.discr e.toModel = 0