Hola,
Estoy tratando de hacer este ejercicio que pide probar la transitividad de LE (menor o igual). ¿La idea es hacer inducción y luego aplicar inversión para poder demostrarlo? Porque no estoy pudiendo.
Saludos,
Jairo.
Hola.
Si, la idea es usar inducción en un nat o en LE.
Se usa también inversion (o inversion_clear), inversion Hi in Hj (o inversion_clear Hi in Hj ) y constructor.
Saludos, Carlos