Hi

What is the names of the following theorems

```
forall n:nat, S n = 0 -> False.
forall (n,m:nat), S n = S m -> n = m.
```

How can I find them myself?

```
Require Import Arith.
(* forall n:nat, S n = 0 -> False. *)
Search (S _ = 0).
(* forall (n,m:nat), S n = S m -> n = m. *)
Search (S _ = S _).
```

Note also that those properties are corollaries of the fact that `S`

and `0`

are constructors. So, you can also use the tactics `discriminate`

and `injection`

, respectively, instead of applying theorems.

Last updated: Jun 20 2024 at 11:02 UTC