English
If x1 and x2 are numeric and IH24 x1 x2 y and IH24 x2 x1 y hold, and x1 ≈ x2, then x1*y ≤ x2*y in the game order.
Русский
Если x1 и x2 числовые, IH24 x1 x2 y и IH24 x2 x1 y выполняются, и x1 ≈ x2, то x1*y ≤ x2*y в порядке игр.
LaTeX
$$$x_1.Numeric \\\\wedge x_2.Numeric \\\\wedge IH24 x_1 x_2 y \\\\wedge IH24 x_2 x_1 y \\\\Rightarrow \\\\mathrm{le}(instHMul.hMul x_1 y, instHMul.hMul x_2 y)$$$
Lean4
/-- P2 follows from specialized induction hypotheses (one half of the equality). -/
theorem mul_right_le_of_equiv (h₁ : x₁.Numeric) (h₂ : x₂.Numeric) (h₁₂ : IH24 x₁ x₂ y) (h₂₁ : IH24 x₂ x₁ y)
(he : x₁ ≈ x₂) : x₁ * y ≤ x₂ * y := by
have he' := neg_equiv_neg_iff.2 he
apply PGame.le_of_forall_lt <;> simp_rw [lt_iff_game_lt]
· rw [leftMoves_mul_iff (_ > ·)]
refine ⟨mulOption_lt_mul_of_equiv h₁ h₁₂ he, ?_⟩
rw [← quot_neg_mul_neg]
exact mulOption_lt_mul_of_equiv h₁.neg (ih24_neg <| (ih24_neg h₂₁).1).2 he'
· rw [rightMoves_mul_iff]
constructor <;> intros <;> rw [lt_neg]
· rw [← quot_mul_neg]
apply mulOption_lt_mul_of_equiv h₂ (ih24_neg h₂₁).2 (symm he)
· rw [← quot_neg_mul]
apply mulOption_lt_mul_of_equiv h₂.neg (ih24_neg h₁₂).1 (symm he')
