Buenos dias!
En el ejercicio 6.5 del práctico 6, parte 3, se recomienda usar la táctica Omega para la resolución de las inegualdades planteadas. En la documentación de Coq (https://coq.github.io/doc/v8.13/refman/addendum/omega.html) hay una advertencia de que esta táctica ha sido deprecada, y se recomienda utilizar la táctica "lia" (https://coq.github.io/doc/v8.13/refman/addendum/micromega.html#lia-a-tactic-for-linear-integer-arithmetic). Además, al intentar importar Omega (Require Import Omega.) estoy obteniendo el siguiente error:
Cannot find a physical path bound to logical path Omega.
Quería consultar si se podia utilizar la táctica lia en vez de omega en este ejercicio. Muchas gracias!