data NatList : ℕ -> Set where
  [] : NatList 0
  _::_ : {n : ℕ} -> ℕ -> NatList n -> NatList (suc n)



insert : {n : ℕ} -> ℕ -> NatList n -> NatList (suc n)
insert e [] = e :: []
insert e (a :: l) with (e ≤? a)
... | yes _  =  e :: (a :: l)
... | no _ =  a :: (insert e l)