```
Theorem a_value : forall (a:nat),
a - 1 + 1 = a.
```

To solve above ,which lemma (related to minus sign between two terms ) i should apply here?

That's not true if a = 0.

Note that this theorem is wrong if `a = 0`

, since `0 - 1 = 0`

. If you use mathcomp, you can find a lemma to prove the following variant:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Theorem a_value : forall (a:nat),
0 < a -> a - 1 + 1 = a.
Proof.
move=> a lt0a.
Search (_ - ?n + ?n).
by rewrite subnK.
Qed.
```

Last updated: Feb 08 2023 at 23:03 UTC