turn inequality of the natural numbers to cases

Stream: new members

[Kevin Buzzard]

Another tip: don't ever use > or ≥. All the lemmas in the library are stated for < and \le, because it would double the length of the inequality API if we also put lemmas with > and \ge in. Tools like library_search might miss lemmas if you're using > instead of < (it might be smart enough to realise but it's good practice anyway).

[Kevin Buzzard]

Siyuan Yan said:

thanks! I gotta be more familiar with the libraries

The tricks here: (a) start to understand what to expect in the library and what not to expect, for example 2*x+4*y=2*(x+2*y) is true but not a good library lemma (this should be proved with a high-powered tactic like ring), but if x : nat then x <= 0 -> x = 0 and x < 1 -> x = 0 would be good library lemmas because you can imagine them coming up again and again.

(b) start to learn the conventions for naming lemmas in the library. For example all notations have names -- <= is le, < is lt and so on. The naming convention link on the community website gives tons of hints. The logic behind Ruben's correct guess above is: they knew that the statement a < 1 <-> a = 0 would be useful for you and might well be in the library, so they guessed what that lemma would be called based on the naming convention and they guessed correctly. We don't all carry around the names of all 100,000 lemmas in mathlib in our heads, but "power users" understand the naming convention well and use it to make writing code easier.

[Siyuan Yan]

that makes sense!