Bolton Bailey (Jun 05 2022 at 18:09): Bolton Bailey (Jun 05 2022 at 18:09):Hey I am wanting to use the fact that for natural numbers, 0 = a - b <-> a <= b. Is this in the standard library somewhere?
Incidentally, what's the best way to search for a lemma like this? The ideal for me would be some kind of search bar where I can type in "nat sub eq zero iff le" and potentially get a result. There's this index but this requires you to input the first letter of the declaration you want, and is not really searchable.
Li-yao (Jun 05 2022 at 18:12):Search Nat.sub O eq iff.
Ana de Almeida Borges (Jun 05 2022 at 18:50):Search is very powerful but also very literal, so it can take some skill to use well. See the examples in the refman for inspiration.
Ana de Almeida Borges (Jun 05 2022 at 18:53):Some advice from my experience: if you're looking for a lemma that should exist but can't find it, try widening your net, by either removing search terms or being less specific. For example, Search (0 = _ - _) is more specific than Search 0 (_ - _).
Last updated: Oct 13 2024 at 01:02 UTC