[Agda] Positive numbers

[J.Burton at brighton.ac.uk]

Hi, sorry for such a basic question, but I'm confused as to why I
can't make a type of numbers > 0 as below. The error seems to be
re. the pattern matching in the signature of pos. 

data N : Set where
  zero : N
  succ : N -> N

data N+ : N -> Set where
  pos : forall {n : N} -> (succ n) -> N+

Error:
N !=< _33
when checking that the expression succ n has type _33

------------------------

Thanks,

Jim