walker (Oct 19 2022 at 22:17): walker (Oct 19 2022 at 22:17):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).
Paolo Giarrusso (Oct 20 2022 at 01:30):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