Nat.find

def Units.NatFind.find {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) : ℕ

Alternative definition of Nat.find using tail recursion.

Equations

• Units.NatFind.find H = (Units.NatFind.findX✝ H).val

theorem Units.NatFind.find_spec {p : ℕ → Prop} [DecidablePred p] (H : ∃ (n : ℕ), p n) : p (find H)