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⟩
case cons
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
h : maxNormSuccOnSupp norm crds (head :: tail) > 0
⊢ ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds (head :: tail) = norm x + 1
no goals