find_comp_succ — Mathlib

English

If there exist n with p(n) and n+1 with p(n+1) and not p(0), then the smallest witness shifts by one: find h1 equals find h2 plus one.

Русский

Если существуют n с p(n) и n+1 с p(n+1) и не выполняется p(0), то наименьшее решение сдвигается на единицу: find h1 = find h2 + 1.

LaTeX

$$$\\mathrm{Nat.find}(h_1) = \\mathrm{Nat.find}(h_2) + 1.$$$

Lean4

theorem find_comp_succ (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h0 : ¬p 0) : Nat.find h₁ = Nat.find h₂ + 1 :=
  by
  refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩
  cases n
  exacts [h0, @Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]

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