Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
g : Γ
h : coeff x g ≠ 0
⊢ order x ≤ g
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
g : Γ
h : coeff x g ≠ 0
⊢ ↑(addVal Γ R) x ≤ ↑g
rw [addVal_apply_of_ne (ne_zero_of_coeff_ne_zero h), WithTop.coe_le_coe]
no goals
Γ : Type u_1
R : Type u_2
inst✝² : LinearOrderedCancelAddCommMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x : HahnSeries Γ R
g : Γ
h : coeff x g ≠ 0
⊢ order x ≤ g
exact order_le_of_coeff_ne_zero h