So far `eqP`

and friends are amazing when I have to do them once or twice (usually for f_equal)

But I am in a situation where I have list of hypothesis that are all using ssrnat, and goal that is in the same way. I know lia can solve it, but I was looking for a nice way to do it (or if ssreflect has alternative to lia that will automatically solve all nat goals).

I think https://github.com/math-comp/mczify was the most recent effort for this? (The math-comp stream might have better answers)

Last updated: Sep 30 2023 at 05:01 UTC