English
If q implies p for all n, then the least witness of p is at least as large as that of q, i.e., Nat.find(h_p) ≤ Nat.find(h_q).
Русский
Если $q(n) \\Rightarrow p(n)$ для всех $n$, то наименьшее решение $p$ не превосходит наименьшее решение $q$; то есть Nat.find(h_p) ≤ Nat.find(h_q).
LaTeX
$$$\\mathrm{Nat.find}(hp) \\le \\mathrm{Nat.find}(hq).$$$
Lean4
/-- If a predicate `q` holds at some `x` and implies `p` up to that `x`, then
the earliest `xq` such that `q xq` is at least the smallest `xp` where `p xp`.
The stronger version of `Nat.find_mono`, since this one needs
implication only up to `Nat.find _` while the other requires `q` implying `p` everywhere. -/
theorem find_mono_of_le [DecidablePred q] {x : ℕ} (hx : q x) (hpq : ∀ n ≤ x, q n → p n) :
Nat.find ⟨x, show p x from hpq _ le_rfl hx⟩ ≤ Nat.find ⟨x, hx⟩ :=
Nat.find_min' _ (hpq _ (Nat.find_min' _ hx) (Nat.find_spec ⟨x, hx⟩))
