Zulip Chat Archive

Stream: new members

Topic: le_succ_self

Alan Post (Dec 06 2021 at 11:50):

In Inequality World, level 10, le_succ_self, the description says "Can you find the two-line proof?"

I was surprised by this, because while I've found the Natural Number Game quite challenging in general, I thought the one-line proof "exact le_succ a a (le_refl a)," was the obvious way to go for this one.

Ruben Van de Velde (Dec 06 2021 at 12:00):

That's a good proof, indeed. Perhaps it means "the two-line proof without using earlier lemmas"

Eric Wieser (Dec 06 2021 at 12:05):

Looking at the answers, that is indeed what it means

Alan Post (Dec 06 2021 at 13:07):


Kevin Buzzard (Dec 06 2021 at 19:44):

It's always nice to be golfed :-) You should open an issue saying you found a 1 line proof and want your money back :-)

Alan Post (Dec 07 2021 at 01:26):

I'm very appreciative of the Natural Number Game, and will happily pay full price for any sequels. :grinning:

Last updated: Dec 20 2023 at 11:08 UTC