tactic for inequality calculation?

Stream: lean4

[Dean Young]

def p : -7 < 9 := sorry

def p : -7 ≤ 11 := sorry

[Mario Carneiro]

norm_num

[Martin Dvořák]

Is decide inferior?

[Mario Carneiro]

decide will also work, but it is more limited and might not use the best algorithms

[Mario Carneiro]

norm_num uses decide when it is beneficial

[Mario Carneiro]

decide won't work to evaluate inequalities of reals

[Eric Wieser]

@Kind Bubble, note these should be theorem not def

[Dean Young]

thanks!