-- inserts a number n at the n-th position in the list
insert :: Nat -> [Nat] -> [Nat]
insert x [] = [x]        
insert Z [S Z] = [Z,S Z]
insert Z [S(S Z)] = [Z,S(S Z)]
insert (S Z) [Z] = [Z,(S Z)]
insert (S Z) [S(S Z)] = [S Z, S(S Z)]
insert (S(S Z)) [Z] = [Z, S(S Z)]
insert (S(S Z)) [S Z] = [S Z, S(S Z)]        
insert Z [S Z, S(S Z)] = [Z, S Z, S(S Z)]
insert (S Z) [Z,S(S Z)] = [Z, S Z, S(S Z)]
insert (S(S Z)) [Z, S Z] = [Z, S Z, S(S Z)]