English
If k is a left move of x*y, then k comes either from a left-move combination (Sum.inl) or a right-move combination (Sum.inr) of the factors; equivalently, every left move of x*y arises from one of these two structured sources.
Русский
Если k является левым ходом x*y, то он возникает либо из левого сочетания ходов, либо из правого сочетания ходов; другими словами, каждый левый ход x*y получен из одного из двух структурированных источников.
LaTeX
$$$$k \\in (x*y).LeftMoves \\Rightarrow (\\exists i,j\\, k = toLeftMovesMul(\\mathrm{Sum.inl}(i,j)) \\,\\lor\\, \\exists jx, jy\\, k = toLeftMovesMul(\\mathrm{Sum.inr}(jx,jy))).$$$$
Lean4
@[simp]
theorem neg_mk_mul_moveRight_inl {xl xr yl yr} {xL xR yL yR} {i j} :
(-(mk xl xr xL xR * mk yl yr yL yR)).moveRight (Sum.inl (i, j)) =
-(xL i * mk yl yr yL yR + mk xl xr xL xR * yL j - xL i * yL j) :=
rfl
