English
Insertion on the left and on the right commutes: inserting x first to the left of x' and then x'' on the right is the same game as inserting x' on the right of x'' and then x on the left against them. In symbols: insertRight(insertLeft x x') x'' = insertLeft(insertRight x x'') x'.
Русский
Вставка слева и вставка справа коммутируют: получить одну и ту же игру можно, вставив сначала слева x слева от x', затем справа x''; или наоборот.
LaTeX
$$$ \\mathrm{insertRight}(\\mathrm{insertLeft}(x,x'),x'') = \\mathrm{insertLeft}(\\mathrm{insertRight}(x,x''),x'). $$$
Lean4
/-- Inserting on the left and right commutes. -/
theorem insertRight_insertLeft {x x' x'' : PGame} :
insertRight (insertLeft x x') x'' = insertLeft (insertRight x x'') x' :=
by
cases x; cases x'; cases x''
dsimp [insertLeft, insertRight]
