Which lemma from standard libray may be helpful in the following condition

```
(a1 + 1 <=? b) && k1<=k2 && k3<=k4
(a1 - 1 <=? b) && k1<=k2 && k3<=k4
```

Could you also include the code giving the error? Could help people understand what's the error is about better.

I want to prove above relation . lt from library may helpful in proving the above relation? Secondly, (destruct <=) gives error.

You should transform your goal before applying `Nat.ltb_lt`

.

```
repeat rewrite Bool.andb_true_iff. repeat rewrite Nat.ltb_lt.
```

Last updated: Jan 31 2023 at 14:03 UTC