Zulip Chat Archive

Stream: new members

Topic: introduce new numbers


Lu-Ming Zhang (May 21 2021 at 08:48):

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 (May 21 2021 at 08:57):

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 (May 21 2021 at 08:58):

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

Eric Rodriguez (May 21 2021 at 08:59):

i did not know generalize could do that wow


Last updated: Dec 20 2023 at 11:08 UTC