What is the idiomatic way to discharge False from hypotheses like S n = n, or S (S n) = n? Right now it seems like I need to prove a lemma for each of those, which makes me think that either I encountered a bug or I am missing something.

`lia`

should work:

```
From Coq Require Import Lia.
Goal forall n, S n = n -> False.
Proof. lia. Qed.
```

*Disclaimer: not tested, may not compile*

Thank you, I don't think I would have figured that out on my own. I learned Agda first, and my instinct is to try to get the type checker to fail to unify the terms.

Ethan Day has marked this topic as resolved.

I don't think this would work in Agda simply by utilizing constructor disjointness either.

is this room still active? I had question regarding some proof exercise in cpdt.

although I'm not sure if this is the right place to ask

@kumar You can ask in a new topic.

@Ali Caglayan Thanks!

Last updated: Jun 15 2024 at 05:01 UTC