add_comm — Mathlib

English

`x + y` has exactly the same moves as `y + x`.

Русский

Сумма x + y имеет точно такие же ходы, как и y + x.

LaTeX

$$$ x + y \equiv y + x $$$

Lean4

/-- `x + y` has exactly the same moves as `y + x`. -/
protected theorem add_comm (x y : PGame) : x + y ≡ y + x :=
  match x, y with
  | mk xl xr xL xR, mk yl yr yL yR => by
    refine Identical.of_equiv (Equiv.sumComm _ _) (Equiv.sumComm _ _) ?_ ?_ <;>
      · rintro (_ | _) <;> · dsimp; exact PGame.add_comm _ _
termination_by (x, y)

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