Random obvious thingy

Changes

1 changed files (+12/-0)

• Analysis.lean (new)
  • @@ -0,0 +1,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