Search code examples
coqcoq-tactic

Using "omega" for type "N"

For my research, I wrote a bunch of functions in Coq for the type nat and proved they are correct. Now I need to write the same functions for the type N but proving their correctness seems like a pain since the omega tactic does not work for this type. Is there an alternative for omega on N?

So far I have looked at the library Nnat and found several useful translation from N to nat and vice versa. If no omega alternative exists, is there a tactic to quickly transform a goal in N to nat and use omega on it?

Solution

  • The lia tactic, available in the Lia module, seems to work with N.