0 < 0.1

Stream: new members

[Iocta]

example : 0 < 0.1:= sorry

How to prove this?

[Kevin Buzzard]

I doubt it's true. They're probably both naturals and both 0

[Mario Carneiro]

what type are you talking about?

[Reid Barton]

it can be true, depending on the proof!

[Kevin Buzzard]

You need to explicitly say which 0 you're talking about, otherwise Lean will assume it's a natural

[Mario Carneiro]

aha so it can

[Iocta]

ah, if I : real them, norm_num works

[Mario Carneiro]

if you use theorem then it won't do that

[Jason Orendorff]

oh, 0.1 being interpreted as a natural number seems unfortunate, but I can see why