Oh my, that was insanely helpful, especially the tip on destructing the "larger" hypothesis destruct (H n0)
which gave me a lot more to work with, and the organization of code by a intermediate lemma, Coq can match the induction principle much better that way. Very happy, thanks once again!
Tan Yee Jian has marked this topic as resolved.
Last updated: Jan 27 2023 at 01:03 UTC