concise inequality proofs

Stream: new members

[Scott Olson]

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]

the most concise way is probably to blast it away with a tactic - there are several out there

[Scott Olson]

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

[Johannes Hölzl]

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

[Scott Olson]

You're right, linarith handles it