case tail a as th =>
  rw [maxNormSuccOnSupp]
  let l := supp_below_max norm crds as  x  th h₂ 
  exact if c:crds a ≠ 0 then
    by
    simp [c]
    apply Nat.le_trans l 
    apply snd_le_max
  else
    by 
    simp [c]
    exact l
R : Type u_2
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type u_1
inst✝ : DecidableEq X
norm : X → ℕ
crds : X → R
x : X
h₂ : crds x ≠ 0
a : X
as : List X
th : List.Mem x as
⊢ norm x + 1 ≤ maxNormSuccOnSupp norm crds (a :: as)
no goals