I am converting

(S a) <= b) into boolean form but it is giving error. What could be reason?

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(in the presence of H: b > 0) ? Secondly,

```
(a0+2 <? a1) && (a2 <? a3) && (a4 <? a5) = true
```

I am applying command " try rewrite ltb_lt" , but it is not working.

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

.

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

Last updated: Oct 03 2023 at 21:01 UTC