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: Jan 29 2023 at 05:03 UTC