omega on real?

Stream: new members

[Sorrachai Yingchareonthawornchai]

Hi, do you know why omega cannot solve this?

example {d : ℝ} (hd : 2 ≤ d) : 2 / d ≤ 1 := sorry

[Bolton Bailey]

omega is designed for natural numbers and integers. bound works.

import Mathlib

example {d : ℝ} (hd : 2 ≤ d) : 2 / d ≤ 1 := by bound

[Kevin Buzzard]

Note that you can hover over a tactic in some code and see the description of what it is designed to do.