English
Removing two coordinates in either order yields the same n-tuple.
Русский
Удаление двух координат в любом порядке даёт тот же n-кортеж.
LaTeX
$$$$ i.removeNth (j.removeNth m) = (i.predAbove j).removeNth ((j.succAbove i).removeNth m) $$$$
Lean4
/-- `find p` returns the first index `n` where `p n` is satisfied, and `none` if it is never
satisfied. -/
def find : ∀ {n : ℕ} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)
| 0, _p, _ => none
| n + 1, p, _ => by
exact
Option.casesOn (@find n (fun i ↦ p (i.castLT (Nat.lt_succ_of_lt i.2))) _)
(if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦ some (i.castLT (Nat.lt_succ_of_lt i.2))
