Zulip Chat Archive

Stream: new members

Topic: concise inequality proofs


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Olson (Sep 27 2018 at 09:26):

What are some tactics that might be able to solve this?

view this post on Zulip Johannes Hölzl (Sep 27 2018 at 09:27):

linarith could work. I think it got some support for natural numbers.

view this post on Zulip Scott Olson (Sep 27 2018 at 09:29):

You're right, linarith handles it


Last updated: May 13 2021 at 06:15 UTC