-- drops the first n elements of a list and returns the rest of the list
drop :: Nat -> [a] -> [a]
drop Z             []      = []
drop Z             [a]     = [a]
drop (S Z)         []      = []
drop (S (S Z))     []      = []
drop Z             [a,b]   = [a,b]
drop Z             [a,b,c] = [a,b,c]
drop (S Z)         [a]     = []
drop (S Z)         [a,b]   = [b]
drop (S Z)         [a,b,c] = [b,c]
drop (S (S Z))     [a]     = []
drop (S (S Z))     [a,b]   = []
drop (S (S Z))     [a,b,c] = [c]
drop (S (S (S Z))) []      = []
drop (S (S (S Z))) [a]     = []
drop (S (S (S Z))) [a,b]   = []
drop (S (S (S Z))) [a,b,c] = []