English
If, for all m ≤ n, not P m holds, then n < find P.
Русский
Если для всех m ≤ n верно ¬P(m), то n < find P.
LaTeX
$$$ (n : \mathbb{N}) \ (\forall m \le n, \neg P(m)) \Rightarrow (n : \mathrm{PartENat}) < \mathrm{find}(P) $$$
Lean4
theorem lt_find (n : ℕ) (h : ∀ m ≤ n, ¬P m) : (n : PartENat) < find P :=
by
rw [coe_lt_iff]
intro h₁
rw [find_get]
have h₂ := @Nat.find_spec P _ h₁
revert h₂
contrapose!
exact h _