H: a<b goal : a<?b=true
Why i cannot apply H directly?
The goal and
H have different types. You can use
Let's add that you should be cautious not to take
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
Last updated: Feb 01 2023 at 12:30 UTC