# Zulip Chat Archive

## Stream: maths

### Topic: proving less than

#### bulut buyru (Mar 28 2019 at 02:33):

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 (Mar 28 2019 at 03:26):

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 (Mar 28 2019 at 03:28):

what do I need to import to use norm_num?

#### Scott Morrison (Mar 28 2019 at 03:29):

`import tactic.norm_num`

, assuming you have `mathlib`

installed.

#### Bryan Gin-ge Chen (Mar 28 2019 at 03:30):

Yeah, oops, forgot to put the import in!

#### bulut buyru (Mar 28 2019 at 03:47):

thanks !

Last updated: May 18 2021 at 06:15 UTC