Negated proof on else-branch

Stream: new members

[Marcus Rossel]

If-then-else expressions give us the option of obtaining a proof of the condition we're checking on the then-branch:

if h : my_condition
then use_condition h
else ...

Is there a way of obtaining a proof of ¬h on the else-branch?

[Alex J. Best]

In the else branch the identifier h should refer to a term of type ¬my_condition