How can one prove a simple (in)equality in reals?

Stream: mathlib4

[Jihoon Hyun]

I'm talking about things like 0 ≤ 5 or -2 < 2 over the reals.
There should be an easy way, but decide and several other things which worked with natural numbers doesn't work with reals.

[Martin Dvořák]

linarith

[Jihoon Hyun]

interesting..

[Eric Rodriguez]

norm_num?