I have the hypothesis
H : N s = 0
and I want to prove the following
~ (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: Jan 29 2023 at 01:02 UTC