English
If x = y + single x.order x.leadingCoeff and y ≠ 0, then x.order < y.order.
Русский
Если x = y + единичный член в порядке x.order и y ≠ 0, то x.order < y.order.
LaTeX
$$$$ x.order < y.order \quad \text{given } x = y + \operatorname{single}(x.order) x.leadingCoeff \text{ and } y \neq 0. $$$$
Lean4
theorem order_lt_order_of_eq_add_single {R} {Γ} [LinearOrder Γ] [Zero Γ] [AddCancelCommMonoid R] {x y : HahnSeries Γ R}
(hxy : x = y + single x.order x.leadingCoeff) (hy : y ≠ 0) : x.order < y.order :=
by
have : x.order ≠ y.order := by
intro h
have hyne : single y.order y.leadingCoeff ≠ 0 := single_ne_zero <| leadingCoeff_ne_zero.mpr hy
rw [leadingCoeff_eq, ← h, coeff_order_of_eq_add_single hxy, single_eq_zero] at hyne
exact hyne rfl
refine lt_of_le_of_ne ?_ this
simp only [order, ne_zero_of_eq_add_single hxy hy, ↓reduceDIte, hy]
have : y.support ⊆ x.support := by
intro g hg
by_cases hgx : g = x.order
· refine (mem_support x g).mpr ?_
have : x.coeff x.order ≠ 0 := coeff_order_ne_zero <| ne_zero_of_eq_add_single hxy hy
rwa [← hgx] at this
· have : x.coeff g = (y + (single x.order) x.leadingCoeff).coeff g := by rw [← hxy]
rw [coeff_add, coeff_single_of_ne hgx, add_zero] at this
simpa [this] using hg
exact Set.IsWF.min_le_min_of_subset this
