convert equality to inequality

Stream: new members

[Lu-Ming Zhang]

In the NNG, if I have
a b c:mynat
h: b=a+c (or h: b=a+0),
How to convert h to a<=b or introduce a new hypothesis a<=b?

[Kevin Buzzard]

you could put have h2 : a <= b and then you'll get a new goal which you can prove using h.

[Lu-Ming Zhang]

Kevin Buzzard said:

you could put have h2 : a <= b and then you'll get a new goal which you can prove using h.

In the NNG, I put have h2 : a <= b, then I only got h2 : Prop. Why is that?

[Lu-Ming Zhang]

By the way, how to input letters like ℕ in Lean?

[Eric Wieser]

It sounds like you wrote have h2 := a <= b not have h2 : a <= b.

[Eric Wieser]

Vscode lets you type \nat to get ℕ

[Lu-Ming Zhang]

Many thanks to Eric and Kevin!