Stream: Coq users

Topic: ✔ None <> Some a


view this post on Zulip Mathieu Dehouck (Jan 25 2022 at 13:49):

Dear All,
I am renew to Coq, and after a lot of struggle, I start to get my way through.
I have a new silly problem : a proof where the goal is "None <> Some a".
Is there a tactic or a lemma somewhere I could use to solve it?
I've looked around, and tried trivial, simpl, auto... I can't seem to find the point.
Best.

view this post on Zulip Gaëtan Gilbert (Jan 25 2022 at 13:51):

discriminate should work

view this post on Zulip Mathieu Dehouck (Jan 25 2022 at 14:01):

perfectly so.
Thank you

view this post on Zulip Notification Bot (Jan 25 2022 at 14:01):

Mathieu Dehouck has marked this topic as resolved.


Last updated: Mar 28 2024 at 15:01 UTC