English
If hy is numeric and the IHs hold in both orders, then whenever x.moveLeft i < x.moveLeft j, the corresponding mulOption terms are ordered as in the statement of the theorem.
Русский
Если hy численно, и IH в обоих направлениях выполняются, то при x.moveLeft i < x.moveLeft j выполняется требуемая линейность mulOption.
LaTeX
$$$\\forall {x y} \\ hy \\ IH1 x y \\ IH1 y x \\forall i \\forall j \\forall k \\forall l \\; (x.moveLeft i) < (x.moveLeft j) \\Rightarrow (\\mathrm{mulOption} x y i k) < -(\\mathrm{mulOption} x (-y) j l)$$$
Lean4
theorem mulOption_lt_of_lt (hy : y.Numeric) (ihxy : IH1 x y) (ihyx : IH1 y x) (i j k l)
(h : x.moveLeft i < x.moveLeft j) : (⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧ :=
mulOption_lt_iff_P1.2 <| P1_of_lt (P3_of_ih hy ihyx j k l) <| ((P24_of_ih ihxy i j).2 h).1 k
