# Beginner: stuck on simple proof with negation

**URL:** <https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886>\
**Category:** Miscellaneous\
**Created:** [December 20, 2025, 1:25pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886 "2025-12-20T13:25:59Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![ReiHakiri](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/reihakiri/32/1212_2.png) [@ReiHakiri](https://discourse.rocq-prover.org/u/ReiHakiri)\
**Post date:** [December 20, 2025, 1:25pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886/1 "2025-12-20T13:25:59Z")

</div>

Hello, I just started learning Coq and I’m trying to prove the following thm.

> \neg \exists n: nat, \forall m: nat, n = m

Here’s my attempt:

```auto
Theorem attempt: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  specialize (H (S n)).
  discriminate H. (* Doesn't work *)

```

Why can I not use discriminate here? What is the correct proof for this?

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [December 20, 2025, 1:37pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886/2 "2025-12-20T13:37:14Z")

</div>

The `discriminate` tactic is useful when both sides of an equality start with different constructors, which is not the case here. In your case, the proof needs to be a bit more involved, as the contradiction comes from the recursive structure of natural numbers. So, before you can meaningfully use `discriminate` (or `injection`), you need to perform a proof by induction on `n` to consider the various ways `n` can be built.

---

<div class="post-metadata">

**Author:** ![ReiHakiri](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/reihakiri/32/1212_2.png) [@ReiHakiri](https://discourse.rocq-prover.org/u/ReiHakiri)\
**Post date:** [December 20, 2025, 1:58pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886/3 "2025-12-20T13:58:37Z")

</div>

Thanks for your help! Here’s the code that worked:

```auto
Theorem attempt: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  specialize (H (S n)).
  induction n as [| n' IH].
    - discriminate H.
    - inversion H as [H1]. apply IH in H1. assumption.
Qed.

```

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 20, 2025, 2:23pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886/4 "2025-12-20T14:23:24Z")

</div>

Now try proving the same theorem for bool (`~ exists b: bool, forall b’: bool, b = b’`)

---

<div class="post-metadata">

**Author:** ![ReiHakiri](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/reihakiri/32/1212_2.png) [@ReiHakiri](https://discourse.rocq-prover.org/u/ReiHakiri)\
**Post date:** [December 20, 2025, 3:10pm UTC](https://discourse.rocq-prover.org/t/beginner-stuck-on-simple-proof-with-negation/2886/5 "2025-12-20T15:10:46Z")

</div>

Thanks for your exercise. After it, I realized that using specialize inside destruct cases removes the need to use induction on n for the original proof:

```auto
Theorem no_single_nat: ~ exists n: nat, forall m: nat, n = m.
Proof.
  unfold not.
  intros H.
  destruct H as [n H].
  destruct n as [| n'].
  - specialize (H 1). discriminate.
  - specialize (H 0). inversion H.
Qed.

```