simpler tactic than linarith for < > comparisons? (beginner)

Stream: new members

[rzeta0]

The following is a very simple proof that if $a=4$ then $a>1$.

-- 01 - First Proof

import Mathlib.Tactic

example {a: ℕ} (h1: a = 4) : a > 1 := by linarith

The linarith tactic, as far as I can tell does a lot more than justify ordering in the natural numbers. The docs tell me is does more sophisticated linear algebra.

My question therefore is - is there a simpler, smaller, tactic that can prove the above? Something that just encodes the ordering on the natural numbers, integers, reals, perhaps? Is there a "inequalities" tactic?

[Rida Hamadani]

Perhaps omega is a special case of what you want, that works only for natural numbers. Replacing linarith by omega in your proof reduces its time to less than 10%.