English
If x1 numeric, IH24 x1 x2 y, and x1 ≈ x2, then for any i in x1.LeftMoves and j in y.LeftMoves, mulOption x1 y i j is strictly less than the product x2*y.
Русский
Если x1 численно, IH24 x1 x2 y и x1 эквивалентно x2, то для любых i из leftMoves x1 и j из leftMoves y, mulOption x1 y i j < x2*y.
LaTeX
$$$x_1.Numeric \\\\wedge\\\\ IH24 x_1 x_2 y \\\\wedge\\\\ x_1 \\\\approx x_2 \\\\Rightarrow\\\\forall (i: x_1.LeftMoves) (j: y.LeftMoves),\\\\lt(Quotient.mk SetTheory.PGame.setoid (x_1.mulOption y i j)) (Quotient.mk SetTheory.PGame.setoid (instHMul.hMul x_2 y))$$$
Lean4
theorem numeric_of_ih (ih' : ∀ a, ArgsRel a (Args.P24 x₁ x₂ y) → P124 a) : (x₁ * y).Numeric ∧ (x₂ * y).Numeric :=
by
constructor <;> refine ih' (Args.P1 _ _) (TransGen.single ?_)
· exact (cutExpand_add_right { y }).2 <| (cutExpand_add_left { x₁ }).2 cutExpand_zero
· exact (cutExpand_add_right { x₂, y }).2 cutExpand_zero
