Stream: new members
Topic: concise inequality proofs
Scott Olson (Sep 27 2018 at 09:07):
How do you approach simple proofs with inequalities like this, concisely? I can always find a way, but it seems like there must be shorter ways.
n : ℕ, h : 1 + n ≤ 1 ⊢ n = 0
Andrew Ashworth (Sep 27 2018 at 09:11):
the most concise way is probably to blast it away with a tactic - there are several out there
Scott Olson (Sep 27 2018 at 09:26):
What are some tactics that might be able to solve this?
Johannes Hölzl (Sep 27 2018 at 09:27):
linarith could work. I think it got some support for natural numbers.
Scott Olson (Sep 27 2018 at 09:29):
linarith handles it
Last updated: May 13 2021 at 06:15 UTC