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):
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.lt. Here are links to some relevant lemmas in lean core and mathlib.
However, the easiest way is probably to use mathlib's
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
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):
Last updated: May 18 2021 at 06:15 UTC