English
Under a swap of indices i and j, the corresponding elements shift in a parity-dependent way.
Русский
При перестановке индексов i и j элементы сдвигаются в зависимости от паритета.
LaTeX
$$$(alternatingWord(i, j, p))[k+1] = (alternatingWord(j, i, p))[k]$ при определённых ограничениях (пометка пропущена) $$
Lean4
theorem getElem_alternatingWord_swapIndices (i j : B) (p k : ℕ) (h : k + 1 < p) :
(alternatingWord i j p)[k + 1]'(by simp [h]) = (alternatingWord j i p)[k]'(by simp; cutsat) :=
by
rw [getElem_alternatingWord i j p (k + 1) (by cutsat), getElem_alternatingWord j i p k (by cutsat)]
by_cases h_even : Even (p + k)
· rw [if_pos h_even, ← add_assoc]
simp only [ite_eq_right_iff, isEmpty_Prop, Nat.not_even_iff_odd, Even.add_one h_even, IsEmpty.forall_iff]
· rw [if_neg h_even, ← add_assoc]
simp [Odd.add_one (Nat.not_even_iff_odd.mp h_even)]
