## 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: May 13 2021 at 06:15 UTC