English
If IH3 x1 (x2.moveLeft i) x2 y1 y2 holds for all i in x2.LeftMoves, and IH3 (-x2) ((-x1).moveLeft i) (-x1) y1 y2 holds for all i in (-x1).LeftMoves, and hl : x1 < x2, then P3 x1 x2 y1 y2.
Русский
Если для всех i из x2.LeftMoves выполняется IH3 x1 (x2.moveLeft i) x2 y1 y2, и для всех i из (-x1).LeftMoves выполняется IH3 (-x2) ((-x1).moveLeft i) (-x1) y1 y2, и hl: x1 < x2, тогда P3 x1 x2 y1 y2.
LaTeX
$$$\\\\forall x_1 x_2 y_1 y_2, \\\\left( \\\\forall i \\\\in x_2.LeftMoves, IH3 x_1 (x_2.moveLeft i) x_2 y_1 y_2 \\\\right) \\\\land \\\\left( \\\\forall i \\\\in (-x_1).LeftMoves, IH3 (-x_2) ((-x_1).moveLeft i) (-x_1) y_1 y_2 \\\\right) \\\\land \\\\left( hl : x_1 < x_2 \right) \\\\Rightarrow P3 x_1 x_2 y_1 y_2.$$$
Lean4
/-- P3 follows from `IH3` (so P4 (with `y₁` a left option of `y₂`) follows from the induction
hypothesis). -/
theorem P3_of_lt {y₁ y₂} (h : ∀ i, IH3 x₁ (x₂.moveLeft i) x₂ y₁ y₂) (hs : ∀ i, IH3 (-x₂) ((-x₁).moveLeft i) (-x₁) y₁ y₂)
(hl : x₁ < x₂) : P3 x₁ x₂ y₁ y₂ :=
by
obtain (⟨i, hi⟩ | ⟨i, hi⟩) := lf_iff_exists_le.1 (lf_of_lt hl)
· exact P3_of_le_left i (h i) hi
· apply P3_neg.2 <| P3_of_le_left _ (hs (toLeftMovesNeg i)) _
simpa
