1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12

import Mathlib

example (x : ℝ) (h : 0 ≤ x) (hn : ∀ n, x ≤ 1 / n) : x = 0 := by
  by_contra
  have := hn <| Nat.ceil (2 / x)
  have : x > 1 / (Nat.ceil (2 / x)) := by
    have := Nat.le_ceil (2 / x)
    have : 1 / x < Nat.ceil (2 / x) := by grind
    have := inv_strictAnti₀ (by grind) this
    field_simp at this
    exact this
  linarith