Stream: Coq users

Topic: How to resolve this?

view this post on Zulip zohaze (Nov 04 2022 at 16:13):

H: x=b
Goal: x<b (while x b are nat).

view this post on Zulip Théo Zimmermann (Nov 04 2022 at 17:49):

Please think of what it means mathematically before attempting to prove something in Coq.

Last updated: Oct 13 2024 at 01:02 UTC