Non-zero Nat is Greater than Zero

Question

In a specific situation, I needed the following proof:

def Nat.zero_lt (n:Nat)(p:n ≠ 0) : 0 < n :=
by
  match n with
  | Nat.zero => contradiction
  | Nat.succ m => simp

That's fine, but I'm wondering if there is a better way of doing this? For example, by using an existing Nat lemma (but I couldn't find a direct match). When faced with a question like this, searching through the Matlib4 documentation does not seem to yield results very easily.