neg_add_cancel_le_zero — Mathlib

English

For any x, -x + x ≤ 0.

Русский

Для любой x выполняется -x + x ≤ 0.

LaTeX

$$$-x + x \le 0$$$

Lean4

theorem neg_add_cancel_le_zero : ∀ x : PGame, -x + x ≤ 0
  | ⟨xl, xr, xL, xR⟩ =>
    le_zero.2 fun i => by
      obtain i | i := i
      · -- If Left played in -x, Right responds with the same move in x.

        refine ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), ?_⟩
        convert @neg_add_cancel_le_zero (xR i)
        apply add_moveRight_inr
      · -- If Left in x, Right responds with the same move in -x.

        dsimp
        refine ⟨@toRightMovesAdd ⟨_, _, _, _⟩ _ (Sum.inl i), ?_⟩
        convert @neg_add_cancel_le_zero (xL i)
        apply add_moveRight_inl

Похожие утверждения