Hola.
No estoy encontrando la forma de nombrar explícitamente las hipótesis que me quedan al usar inversion_clear.
Lo único que encontré fue inversion o inversion_clear as ... pero eso nombra justamente las hipótesis que inversion_clear quita del contexto.
En particular para probar que 4 no es menor o igual a 3 estoy teniendo que usar los nombres automáticos que genera Coq.
Saludos,
Gabriel