Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ coeff x (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x))) ≠ 0
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ coeff x (order x) ≠ 0
rw [order_of_ne hx]
no goals
Γ : Type u_1
R : Type u_2
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
inst✝ : Zero Γ
x : HahnSeries Γ R
hx : x ≠ 0
⊢ coeff x (Set.IsWf.min (_ : Set.IsWf (support x)) (_ : Set.Nonempty (support x))) ≠ 0
exact x.isWf_support.min_mem (support_nonempty_iff.2 hx)