cases Nat.eq_zero_or_pos (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
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
case inl
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) = 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0

case inr
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
h✝ : maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0
⊢ maxNormSuccOnSupp norm (coords s₁) (support s₁) > 0