induction s with
| nil => 
  simp [maxNormSuccOnSupp] at h
| cons head tail ih => 
  exact if c : crds head =0 then
    by 
      simp [maxNormSuccOnSupp, c]
      simp [maxNormSuccOnSupp, c] at h
      exact  ih h
      
  else by    
      simp [maxNormSuccOnSupp, c]
      simp [maxNormSuccOnSupp, c] at h
      let sl := eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
      cases sl
      case inr p =>
          rw [p]
          rw [p] at h
          exact  ih h 
      case inl p =>
          rw [p]
          rw [p] at h
          exact ⟨head, And.intro c rfl⟩
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
no goals