English
Theorem find_comp_succ shows that if p holds for n and not for 1, then find h equals add one to find h2, where h2 witnesses p(n+1).
Русский
Теорема find_comp_succ: если p(n) и p(n+1) существует, и p(1) ложно, тогда find h равно find h2 + 1, где h2 свидетельствует p(n+1).
LaTeX
$$$ \\text{find\_eq\_iff}(h) \Rightarrow \\mathrm{PNat.find}(h) = \\mathrm{PNat.find}(h_2) + 1 $$$
Lean4
theorem find_comp_succ (h : ∃ n, p n) (h₂ : ∃ n, p (n + 1)) (h1 : ¬p 1) : PNat.find h = PNat.find h₂ + 1 :=
by
refine (find_eq_iff _).2 ⟨PNat.find_spec h₂, fun n ↦ ?_⟩
induction n with
| one => simp [h1]
| succ m _ =>
intro hm
simp only [add_lt_add_iff_right, lt_find_iff] at hm
exact hm _ le_rfl
