lemma proved wrapper

`of_nat`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 108lemma of_nat (φ : ℝ) (n : ℕ) : PhiClosed φ (n : ℝ) := by

One-line wrapper that applies simpa.

 109  simpa using of_rat φ n
 110

Lean names referenced from this declaration's body.