simple arithmetic proofs

Stream: new members

[Vincent Siles]

Is there some tactic to discharge simple proofs like example (n: nat) (p: nat) : 2 < 1 + (1 + (1 + (1 + (n + p)))) ? I tried ring and abel but they don't solve it, just simplify the statement

[Johan Commelin]

Maybe omega?

[Rob Lewis]

omega and linarith can both handle that.