English
Let p be a predicate on the natural numbers. 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 q(i) = p(i+1) satisfies q_n + 1 = p_n; equivalently, nth(p(i+1))_n = nth(p)_n − 1 when nth(p)_n ≠ 0.
Русский
Пусть p: ℕ → истина/ложь — предикат на натуральных числах. Если p(0) ложно и n-ый истинный элемент p не равен нулю, то n-ый истинный элемент сдвинутого предиката q(i) = p(i+1) равен p_n − 1; эквивалентно, если nth p n ≠ 0, то nth(p(i+1)) n = 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 {n : ℕ} (h0 : ¬p 0) (h : nth p n ≠ 0) : nth (fun i ↦ p (i + 1)) n + 1 = nth p n :=
nth_add (fun _ hk ↦ (lt_one_iff.1 hk ▸ h0)) h
