How do I "cast" inequalities?

Stream: new members

[YH]

If I have (1 ≤ n) as ℕ how do I get (1:ℝ)≤ ↑n? Library search didn't help.

[Johan Commelin]

norm_cast is supposed to help in such situations

[Kevin Buzzard]

import data.real.basic

example (n : ℕ) (h : 1 ≤ n) : (1 : ℝ) ≤ n :=
begin
  exact_mod_cast h
end

[Kevin Buzzard]

Someone asked me this at Xena yesterday and I revised all the various flavours of norm_cast ;-)