English
For i in Fin(n+1) and j in Fin(n), the parity of i.succAbove j + j.predAbove i equals the parity of i + j.
Русский
Для i∈Fin(n+1) и j∈Fin(n) паритет выражения i.succAbove j + j.predAbove i совпадает с паритетом i + j.
LaTeX
$$$\forall i:\mathrm{Fin}(n+1),\; j:\mathrm{Fin}(n),\; \mathrm{Even}(i.succAbove j + j.predAbove i) \;\iff\; \mathrm{Odd}(i+j).$$$
Lean4
theorem even_succAbove_add_predAbove (i : Fin (n + 1)) (j : Fin n) :
Even (i.succAbove j + j.predAbove i : ℕ) ↔ Odd (i + j : ℕ) :=
by
rcases lt_or_ge j.castSucc i with hji | hij
· have : 1 ≤ (i : ℕ) := (Nat.zero_le j).trans_lt hji
simp [succAbove_of_castSucc_lt _ _ hji, predAbove_of_castSucc_lt _ _ hji, this, iff_comm, parity_simps]
·
simp [succAbove_of_le_castSucc _ _ hij, predAbove_of_le_castSucc _ _ hij, ← Nat.not_even_iff_odd, not_iff,
not_iff_comm, parity_simps]
