given real lt proof rational lt

Stream: Is there code for X?

[Ira Fesefeldt]

I am a bit puzzled, how to prove the following implication involving coes. Anyone a clue how to do that?

import Mathlib

example (x : ℚ) (h : (1:ℝ)/2 < x) : 1/2 < x := sorry

[Riccardo Brasca]

For example

import Mathlib

example (x : ℚ) (h : (1:ℝ)/2 < x) : 1/2 < x := by
  rify [h]

does it

[Riccardo Brasca]

of course you can do it by hand if you prefer

[Ira Fesefeldt]

No, I don't. I just didn't know about rify.

[Ira Fesefeldt]

Thanks!

[Riccardo Brasca]

The key point is docs#Rat.cast_lt