The Natural Numbers Game, lean syntax question

Stream: new members

[Dmitry Mishchenko]

Hello everyone,
I'm new to zulip and lean so please point out any of my misunderstandings. I'm working on the level 9 in the inequality world and here is what I have to prove.
"For all naturals a and b, either a≤b or b≤a."
I know how to prove it mathematically but I don't know how to express it in lean. My "strategy" is using the fact that
(a or b) is equivalent to ((not a) then b)

So here is what I've tried:
by_cases a≤b,
by_cases ∃ (c : mynat), b = a + c,
and in both cases it complains that a proposition I entered is undecidable
Also I think I can't use something like have h := a≤b, because then I have to prove that h is true and it's an impossible goal.
So being desperate I tried to prove a this lemma "(a or b) is equivalent to ((not a) then b)" with "theorem" "begin" and all these commands, but I think I can't do that in the web lean environment.

Please don't tell me that there is this easy way to do this level if I do this that and the other. I want to prove it my way and would really appreciate some help on lean syntax and how to translate my ideas into code or resources that might help me.
Thanks,

[Kyle Miller]

You can rewrite using le_iff_exists_add first and then do cases on that, rather than doing by_cases.

[Kyle Miller]

In more recent versions of Lean, by_cases doesn't complain about undecidable propositions anymore. If you want to simulate it, you can start your proof with the classical tactic, which isn't introduced by the NNG, but it's still present there.

[Patrick Johnson]

Note that you don't need classical logic to solve this level.

[Kyle Miller]

(Just to clarify my classical suggestion -- that's just a workaround to be able to use by_cases for something that should be decidable anyway.)