proving less than

Stream: maths

[bulut buyru]

this is a simple question - but how does one prove that a natural number is >= another natural.
for example, even for something like 1 > 0

[Bryan Gin-ge Chen]

Well, 1>0 follows from the way that > is defined:

example : 1 > 0 := nat.less_than_or_equal.refl 1

There are also tons of already-proven lemmas that are helpful for working with inequalities: if you're using the VS Code extension you'll see a popup filled with suggestions if you start typing e.g. nat.le or nat.lt. Here are links to some relevant lemmas in lean core and mathlib.

However, the easiest way is probably to use mathlib's norm_num tactic:

import tactic.norm_num

example : 173 > 34 := by norm_num

It can handle lots of other arithmetic-related goals. (It looks like norm_num is still not mentioned in the tactics doc?)

[bulut buyru]

what do I need to import to use norm_num?

[Scott Morrison]

import tactic.norm_num, assuming you have mathlib installed.

[Bryan Gin-ge Chen]

Yeah, oops, forgot to put the import in!

[bulut buyru]

thanks !