Commit 2024-12-20 13:13 c800d7a3

feat(Data/Nat/Nth): nth_add_one (#18836) Add the lemma

lemma nth_add_one {n : ℕ} (h0 : ¬p 0) (h : nth p n ≠ 0) :
    nth (fun i ↦ p (i + 1)) n + 1 = nth p n := by

and its variant

lemma nth_add_one_eq_sub {n : ℕ} (h0 : ¬p 0) (h : nth p n ≠ 0) :
    nth (fun i ↦ p (i + 1)) n = nth p n - 1 := by

Feel free to golf; it seems like there ought to be a much shorter proof, possibly following a different approach.