Comparing natural numbers as reals

Stream: new members

[Matei Mandache]

Is there a simple way to compare two natural numbers as reals? In particular, suppose n and m are naturals and we have
h: n ≤ m
is there a way to prove
(n : ℝ) ≤ (m : ℝ)

[Riccardo Brasca]

nat.cast_le works

[Johan Commelin]

norm_cast can do that

[Riccardo Brasca]

I found it with library_search, that for these small lemmas works very well

[Matei Mandache]

Thank you!

[Riccardo Brasca]

also assumption_mod_cast does it