let l := max_in_support norm s₁.coords s₁.support c'
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)
R : Type
inst✝² : Ring R
inst✝¹ : DecidableEq R
X : Type
inst✝ : DecidableEq X
norm : X → ℕ
s₁ s₂ : FormalSum R X
eql : s₁ ≈ s₂
c : ¬maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
c' : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0 :=
  Or.casesOn (motive := fun t =>
    Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁)) = t →
      maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0)
    (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))) (fun h h_1 => h_1.symm ▸ absurd h c)
    (fun h h_1 => h_1.symm ▸ h) (Eq.refl (Nat.eq_zero_or_pos (maxNormSuccOnSupp norm (coords s₁) (support s₁))))
l : ∃ x, coords s₁ x ≠ 0 ∧ maxNormSuccOnSupp norm (coords s₁) (support s₁) = norm x + 1 :=
  max_in_support norm (coords s₁) (support s₁) c'
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) ≤ maxNormSuccOnSupp norm (coords s₂) (support s₂)