How to lift inequality from about Nat to about Real?

Stream: new members

[Ching-Tsun Chou]

If I have (0 : Nat) < n, how do I prove that (0 : Real) < ↑n?

[Matt Diamond]

docs#Nat.cast_pos should rewrite the Real inequality to the Nat one

[Matt Diamond]

the exact_mod_cast tactic also works

[Vlad Tsyrklevich]

Also the rify tactic will do that (there is also zify/qify)

[Yaël Dillies]

Or simply by positivity