English
The order of removing two positions does not affect the resulting sequence.
Русский
Порядок удаления двух позиций не влияет на получившийся кортеж.
LaTeX
$$$$ i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m) $$$$
Lean4
/-- Given an `(n + 2)`-tuple `m` and two indexes `i : Fin (n + 1)` and `j : Fin (n + 2)`,
one can remove `j`th element from `m`, then remove `i`th element from the result,
or one can remove `(j.succAbove i)`th element from `m`,
then remove `(i.predAbove j)`th element from the result.
These two operations correspond to removing the same two elements in a different order,
so they result in the same `n`-tuple. -/
theorem removeNth_removeNth_eq_swap {α : Sort*} (m : Fin (n + 2) → α) (i : Fin (n + 1)) (j : Fin (n + 2)) :
i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m) :=
heq_iff_eq.mp (removeNth_removeNth_heq_swap m i j)
