English
If there are witnesses for p(m+n) and p(n) and n is within the bound, then the index-equation holds: find(h_m) + n = find(h_n).
Русский
Если существуют свидетельства для p(m+n) и p(n) и n не превосходит границы, тогда выполняется равенство индексов: find(h_m) + n = find(h_n).
LaTeX
$$$\\mathrm{Nat.find}(h_m) + n = \\mathrm{Nat.find}(h_n).$$$
Lean4
theorem find_add {hₘ : ∃ m, p (m + n)} {hₙ : ∃ n, p n} (hn : n ≤ Nat.find hₙ) : Nat.find hₘ + n = Nat.find hₙ :=
by
refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
· have hnm : n ≤ m := le_trans hn (find_le hpm)
refine Nat.add_le_of_le_sub hnm (find_le ?_)
rwa [Nat.sub_add_cancel hnm]
· rw [← Nat.sub_le_iff_le_add]
refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
rw [Nat.sub_le_iff_le_add]
exact find_le hpm
