English
If for all k < m we have ¬p k and nth p n ≠ 0, then nth (fun i ↦ p(i+m)) n = nth p n − m.
Русский
Если для всех k < m верно ¬p k и nth p n ≠ 0, тогда nth(p(i+m)) n = nth p n − m.
LaTeX
$$$\\\\forall {p:\\\\mathbb{N}\\\\to \\\\mathsf{Prop}}\\\\ {m n}:\\\\mathbb{N},\\\\ (\\\\forall k < m,\\\\ ¬p k) \\\\Rightarrow \\\\ (\\\\mathrm{nth}\\\\ p\\\\ n \\\\neq 0) \\\\Rightarrow \\\\mathrm{nth}\\\\ (\\\\lambda i\\\\,\\\\ p (i+m))\\\\ n =\\\\ \\mathrm{nth}\\\\ p\\\\ n - m.$$$
Lean4
theorem nth_add_eq_sub {m n : ℕ} (h0 : ∀ k < m, ¬p k) (h : nth p n ≠ 0) : nth (fun i ↦ p (i + m)) n = nth p n - m := by
rw [← nth_add h0 h, Nat.add_sub_cancel]
