Shorten the proof of not_succ_le_self.

ImperialCollegeLondon / natural_number_game

Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.

Apache License 2.0

292 stars 73 forks source link

Closed Julian closed 4 years ago

Julian commented 4 years ago

Not sure if this counts as a nicer proof or not.

It was what I came up with and was shorter than what was here (along with not requiring any branches for subgoals), so figured I'd ask.

Julian commented 4 years ago

Oh. Looks like #93 does the same thing here to this proof.

Closing in favor of that one.