English
Let p be a predicate on the naturals. If p(0) is false and the n-th true value of p is nonzero, then the n-th true value of the shifted predicate p(i+1) satisfies nth(p(i+1))_n = nth(p)_n − 1.
Русский
Пусть p — предикат на натуралых. Если p(0) ложно и n-ый истинный элемент p не равен нулю, то n-ый истинный элемент сдвинтого предиката p(i+1) равен nth p n минус 1.
LaTeX
$$$\\forall p:\\mathbb{N}\\to\\mathcal{P},\\, \\neg p(0) \\land nth(p,n) \\ne 0 \\Rightarrow nth(p(\\cdot+1),n) = nth(p,n) - 1$$$
Lean4
theorem 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 :=
nth_add_eq_sub (fun _ hk ↦ (lt_one_iff.1 hk ▸ h0)) h
