English
If x1 < x2 and y1 < y2 with x1, x2, y1, y2 numeric, then P3 x1 x2 y1 y2 holds.
Русский
Если x1 < x2 и y1 < y2 при условии, что x1, x2, y1, y2 числовые, то выполняется P3(x1, x2, y1, y2).
LaTeX
$$$$ \forall x_1\,x_2\,y_1\,y_2\; (x_1.Numeric \land x_2.Numeric \land y_1.Numeric \land y_2.Numeric \land x_1 < x_2 \land y_1 < y_2) \Rightarrow P3(x_1,x_2,y_1,y_2). $$$$
Lean4
/-- One additional inductive argument that supplies the last missing part of Theorem 8. -/
theorem P3_of_lt_of_lt (hx₁ : x₁.Numeric) (hx₂ : x₂.Numeric) (hy₁ : y₁.Numeric) (hy₂ : y₂.Numeric) (hx : x₁ < x₂)
(hy : y₁ < y₂) : P3 x₁ x₂ y₁ y₂ := by
revert x₁ x₂
rw [← Prod.forall']
refine (wf_isOption.prod_gameAdd wf_isOption).fix ?_
rintro ⟨x₁, x₂⟩ ih hx₁ hx₂ hx
refine P3_of_lt ?_ ?_ hx <;> intro i
· have hi := hx₂.moveLeft i
exact
⟨(P24 hx₁ hi hy₁).1, (P24 hx₁ hi hy₂).1, P3_comm.2 <| ((P24 hy₁ hy₂ hx₂).2 hy).1 _,
ih _ (snd <| IsOption.moveLeft i) hx₁ hi⟩
· have hi := hx₁.neg.moveLeft i
exact
⟨(P24 hx₂.neg hi hy₁).1, (P24 hx₂.neg hi hy₂).1, P3_comm.2 <| ((P24 hy₁ hy₂ hx₁).2 hy).2 _,
by
rw [moveLeft_neg, ← P3_neg, neg_lt_neg_iff]
exact ih _ (fst <| IsOption.moveRight _) (hx₁.moveRight _) hx₂⟩
