English
Under numeric assumptions hx, hy and IHs in both directions, for all i,j,k,l the corresponding mulOption inequalities hold between x*y and x*(-y).
Русский
При числовых предпосылках hx, hy и IH в обоих направлениях выполняются неравенства mulOption между x*y и x*(-y) для любых i,j,k,l.
LaTeX
$$$\\\\forall x y, x.Numeric \\\\Rightarrow y.Numeric \\\\Rightarrow IH1 x y \\\\Rightarrow IH1 y x \\\\Rightarrow \\\\forall i j k l, \\\\mathrm{lt}(Quotient.mk SetTheory.PGame.setoid (x.mulOption y i k)) \\\\lt (Quotient.mk SetTheory.PGame.setoid (x.mulOption (SetTheory.PGame.instNeg.neg y) j l))$$$
Lean4
theorem mulOption_lt (hx : x.Numeric) (hy : y.Numeric) (ihxy : IH1 x y) (ihyx : IH1 y x) (i j k l) :
(⟦mulOption x y i k⟧ : Game) < -⟦mulOption x (-y) j l⟧ :=
by
obtain (h | h | h) := lt_or_equiv_or_gt (hx.moveLeft i) (hx.moveLeft j)
· exact mulOption_lt_of_lt hy ihxy ihyx i j k l h
· have ml := @IsOption.moveLeft
exact
mulOption_lt_iff_P1.2
(P1_of_eq h (P24_of_ih ihxy i j).1 (ihxy (ml i) (ml j) <| Or.inr <| isOption_neg.1 <| ml l).1 <|
P3_of_ih hy ihyx i k l)
· rw [mulOption_neg_neg, lt_neg]
exact mulOption_lt_of_lt hy.neg (ih1_neg_right ihxy) (ih1_neg_left ihyx) j i l _ h
