The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 02/07/2018 10:56 AM, 
fritjof AT uni-bremen.de
 wrote:
> Can someone point me into the right direction or do I oversee something?

you have to prove an equivalence A <-> B, a way to do it is to prove A
-> B and B -> A. This is done by split


One direction is easy if None = Some _ -> _

this assumption is impossible , using the tactic discriminate for example


In the other direction we have  a context that is contradictory
something like

h1 : a < b
h2 : b <= c

In this case you can point the contradiction by using the tactic
contradict  (ccontradict h1 or contradict h2)

and use a theorem about order and negation.

Search _ (_ <= _)  (~ _).


--
Laurent