[Agda] suc _ > 0

[Sergei Meshveliani]

People,
It is often needed to provide  y>0 : y > 0   for   y = suc _
(y : ℕ).

Using  lib-0.7,  I write    s≤s z≤n   in place of  y>0.

Then, I see that this is not so readable, and I replace this further
with  
     suc>0,

with adding the function

  suc>0 : ∀ {m} → suc m > 0
  suc>0 = s≤s z≤n

But may be I am missing something simple in the library?

Thanks,

------
Sergei