Hi,

I have the hypothesis

H : N s = 0

and I want to prove the following

______________________________________(1/2)

~ (exists t : nat, R s t /\ t < s)

My idea was to assume that 't' exists and reach a contradiction by showing that in that case N s should be less than 0. Which tactic should I use?

A link to a document with examples of proofs by contradiction in Coq would be also very helpful.

Many thanks in advance.

The way negation is constructed in Coq is by saying `~ A := A -> False`

. So to show your goal you can begin by introducing some hypothesis of type `exists t : nat, R s t /\ t < s`

using `intro h`

for instance.

this may be useful to understand the default Coq behavior for contradiction: https://existentialtype.wordpress.com/2017/03/04/a-proof-by-contradiction-is-not-a-proof-that-derives-a-contradiction/

Last updated: Sep 28 2023 at 11:01 UTC