Zulip Chat Archive

Stream: maths

Topic: proving less than


view this post on Zulip 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

view this post on Zulip 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?)

view this post on Zulip bulut buyru (Mar 28 2019 at 03:28):

what do I need to import to use norm_num?

view this post on Zulip Scott Morrison (Mar 28 2019 at 03:29):

import tactic.norm_num, assuming you have mathlib installed.

view this post on Zulip Bryan Gin-ge Chen (Mar 28 2019 at 03:30):

Yeah, oops, forgot to put the import in!

view this post on Zulip bulut buyru (Mar 28 2019 at 03:47):

thanks !


Last updated: May 18 2021 at 06:15 UTC