Tri par insertion complet

let rec tri_insertion l =
  match l with
  | [] -> []
  | x :: reste -> insere x (tri_insertion reste)

On trie la queue (plus courte) puis on y insère la tête : l'appel récursif porte sur reste, strictement plus court, d'où la terminaison. La correction repose sur le fait que insere préserve le caractère trié.