introduce new numbers

Stream: new members

[Lu-Ming Zhang]

In the NNG Level 13 of inequality world, I have
a : mynat,
h1 : succ a ≤ a,
h2 : a ≤ succ a
⊢ false
How to introduce a new mynat b to replace succ(a)?

[Eric Rodriguez]

let b := succ a, and then you can use change (...) at (...) to "rewrite" succ a using your new definition. not sure why you'd need this though

[Eric Wieser]

generalize succ a = b I think would also work, as would set b := succ a

[Eric Rodriguez]

i did not know generalize could do that wow