Zulip Chat Archive

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):

You're right, linarith handles it


Last updated: Dec 20 2023 at 11:08 UTC