cast nat in hypothesis to reals

Stream: new members

[Hank]

given (a : nat) (b : nat) and the hypothesis (h : a < b), how do I prove (a:R) < (b:R), which is h casted in the reals? I tried norm_cast but it didn't work.

[Junyan Xu]

Weird, norm_cast should be able to use docs#nat.cast_lt. Can you post a #mwe?