English
From x ⧏ y and numericness of x and y, deduce x ≤ y.
Русский
Из x ⧏ y и числовости x, y следует x ≤ y.
LaTeX
$$$x \le y$ при условии $x \mathbf{LF} y$ и числовости $x$, $y$$$
Lean4
theorem lf_asymm {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y → ¬y ⧏ x :=
by
refine
numeric_rec (C := fun x => ∀ z (_oz : Numeric z), x ⧏ z → ¬z ⧏ x) (fun xl xr xL xR hx _oxl _oxr IHxl IHxr => ?_) x
ox y oy
refine numeric_rec fun yl yr yL yR hy oyl oyr _IHyl _IHyr => ?_
rw [mk_lf_mk, mk_lf_mk]; rintro (⟨i, h₁⟩ | ⟨j, h₁⟩) (⟨i, h₂⟩ | ⟨j, h₂⟩)
· exact IHxl _ _ (oyl _) (h₁.moveLeft_lf _) (h₂.moveLeft_lf _)
· exact (le_trans h₂ h₁).not_gf (lf_of_lt (hy _ _))
· exact (le_trans h₁ h₂).not_gf (lf_of_lt (hx _ _))
· exact IHxr _ _ (oyr _) (h₁.lf_moveRight _) (h₂.lf_moveRight _)
