```
H: a<b
goal : a<?b=true
```

Why i cannot apply H directly?

The goal and `H`

have different types. You can use `Nat.ltb_lt`

.

Let's add that you should be cautious not to take `bool`

for `Prop`

. To sum up, here are the typing relations. Note in particular that `a<b`

is a *type* whereas `a<?b`

is a value, and they don't live in the same sort.

`(a<?b) : bool : Type`

`H : (a<b) : Prop`

`goal : (a<?b = true) : Prop`

Nat.lt_ltb is also possible?

Doesn't that do the opposite conversion?

`Nat.ltb_lt`

is an equivalence. You may use it in both directions. There is no `lt_ltb`

lemma.

Ok,thanks.

Last updated: Sep 28 2023 at 11:01 UTC