rw [p]
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
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = 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
head : X
tail : List X
ih : maxNormSuccOnSupp norm crds tail > 0 → ∃ x, crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds tail = norm x + 1
c : ¬crds head = 0
h : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) > 0
sl : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1 ∨
  max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = maxNormSuccOnSupp norm crds tail :=
  eq_fst_or_snd_of_max (norm head + 1) (maxNormSuccOnSupp norm crds tail)
p : max (norm head + 1) (maxNormSuccOnSupp norm crds tail) = norm head + 1
⊢ ∃ x, ¬crds x = 0 ∧ norm head + 1 = norm x + 1