simp [maxNormSuccOnSupp] at h
case nil
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
h : maxNormSuccOnSupp norm crds [] > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds [] = norm x + 1
no goals