```
S a <= S (S b)->
a < b
```

I am solving it with lia but unable to do it. How i can derive this?

Consider what happens if `a`

and `b`

are `0`

.

Li-Yao is right. The right lemma is :

```
Require Import Lia.
Theorem plop a b : S (S a) <= S b -> a < b.
Proof. lia. Qed.
```

which works (`lia`

is wonderful).

Ok, thanks.

Last updated: Oct 01 2023 at 18:01 UTC