insert : {n : ℕ} -> ℕ -> NatList n -> NatList (suc n)
insert e [] = e :: []
insert e (a :: l) with (e ≤ a)
... | true  =  e :: (a :: l)
... | false =  a :: (insert e l)