It's the traditional, inductive definition of natural numbers. You give a base case (Z = Zero) and an inductive case (S Nat = Successor of Nat). So Z is a natural number, S Z is also a natural number and corresponds to 1, S (S Z) corresponds to 2, etc.