Tan Yee Jian (Dec 07 2022 at 01:25): Tan Yee Jian (Dec 07 2022 at 01:25):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!
Notification Bot (Dec 07 2022 at 01:25):Tan Yee Jian has marked this topic as resolved.
Last updated: Jan 27 2023 at 01:03 UTC