intro h
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
⊢ maxNormSuccOnSupp norm crds s > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
s : List X
h : maxNormSuccOnSupp norm crds s > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1