Several examples show that a contradiction in the goal (like "0 > 0 implies something" when trying to use induction on the length of a list) can be handled by
exfalso. omega.
As the Omega module is deprecated the omega tactic is missing. What is the correct way to handle the mentioned situation?
Thank you
Instead of omega, use lia. See https://coq.inria.fr/doc/v8.13/refman/addendum/omega.html
The
omegatactic is deprecated in favor of theliatactic.