Для моего исследования я написал несколько функций в Coq для типа nat и доказал, что они верны.Теперь мне нужно написать те же функции для типа N, но доказательство их правильности кажется болезненным, поскольку тактика omega не работает для этого типа.Есть ли альтернатива для omega на N?
До сих пор я изучал библиотеку Nnat и нашел несколько полезных переводов из N в nat и наоборот.Если альтернативы omega не существует, существует ли тактика быстрого преобразования цели в N в nat и использования на ней omega?