Hola.
Primero comento que no es un ejercicio trivial y por las dudas aclaro que no se pide en la entrega.
En este caso lo que se pide probar es esencialmente un lema auxiliar que exprese que:
para toda lista L: sorted nat le L -> sorted nat le (insert x L).
Se puede demostrar este lema auxiliar por inducción en L, por ejemplo (también podría ser en la hipótesis sobre: sorted nat le L).
Saludos, Carlos
PD: Ver el libro Coq'Art, written by Yves Bertot and Pierre Casteran.