Goals which are disjunctions

Stream: new members

[Victor Miller]

I'm working my way through the natural number game and have gotten everything except for inequality world 9:
theorem le_total (a b : mynat) : a ≤ b ∨ b ≤ a :=. The problem here is that the goal is a disjunction. Normally, I know that
P \or Q is equivalent to \not P \-> Q, and so I would start with an intro to get \not P in as a hypothesis, but I can't do that. I've fiddled around with trying to introduce \not a \le b as a hypothesis, or do a by_cases on that, but lean says that it isn't decidable. I'm stuck -- what am I missing here? Remember that the natural number game rules are (or should be) restricted to the tactics that are given there.

[Mario Carneiro]

I believe NNG teaches that you can prove a disjunction using left or right

[Kevin Buzzard]

Let P(a) be "for all b, a<=b or b<=a" and prove by induction on a?

[Mario Carneiro]

Of course, you can't start the proof like that because you will get an unsolvable goal, but if you use induction that's how you can finish

[Victor Miller]

That's what I was afraid of. Is it not safe to consider P or Q as equivalent to not P -> Q?

[Kevin Buzzard]

Yes that's the same, probably you can do that in NNG as well, but what is "not a<=b" going to buy you?

[Kevin Buzzard]

it's "for all c, b isn't a + c"

[Victor Miller]

Thanks all. I did finally do it by induction and many cases. The proof was really long!

[Kevin Buzzard]

How long have you been assuming it? ;-)

[Kevin Buzzard]

You're beginning to discover the ugly truth

[Victor Miller]

I remember looking at Russell and Whitehead's Principia a number of years ago and wondering why it was so long. Now I have an idea :-(.

[Kevin Buzzard]

Of course the idea is not that we all recreate the basic interface for the natural numbers -- the idea is that we take the maths that interests us and makes it in the way that mathematicians make it, because all this basic stuff is in the library already.