idxOf_cons_ne — Mathlib

English

If b ≠ a, then idxOf a (b :: l) = succ (idxOf a l).

Русский

Если головной элемент отличен от a, то индекс a в b :: l равен succ (idxOf a l).

LaTeX

$$$ b \neq a \Rightarrow \mathrm{idxOf}(a,\; b :: l) = \mathrm{succ}\big( \mathrm{idxOf}(a, l) \big) $$$

Lean4

@[simp]
theorem idxOf_cons_ne {a b : α} (l : List α) : b ≠ a → idxOf a (b :: l) = succ (idxOf a l)
  | h => by simp only [idxOf_cons, Bool.cond_eq_ite, beq_iff_eq, if_neg h]

Похожие утверждения