import MyNat.Definition
import MyNat.Addition
import AdvancedAdditionWorld.Level1 -- succ_inj
import AdvancedAdditionWorld.Level10 -- zero_ne_succ
namespace MyNat
open MyNat

Advanced Addition World

Level 13: `ne_succ_self`

The last level in Advanced Addition World is the statement that n ≠ succ n.

Lemma

For any natural number n, we have n ≠ succ n.

lemma ne_succ_self: ∀ (n : MyNat), n ≠ succ n
ne_succ_self (n: MyNat
n : MyNat: Type
MyNat) : n: MyNat
n ≠ succ: MyNat → MyNat
succ n: MyNat
n := byn: MyNat
n ≠ succ n
  induction n: MyNat
n withn: MyNat
n ≠ succ n
  | zero: MyNat
zero =>
zerozero ≠ succ zero
    apply zero_ne_succ: ∀ (a : MyNat), 0 ≠ succ a
zero_ne_succGoals accomplished! 🐙
  | succ: MyNat → MyNat
succ n: MyNat
n ih: n ≠ succ n
ih =>n: MyNat
ih: n ≠ succ n
succsucc n ≠ succ (succ n)
    intro hs: succ n = succ (succ n)
hsn: MyNat
ih: n ≠ succ n
hs: succ n = succ (succ n)
succFalse
    apply ih: n ≠ succ n
ihn: MyNat
ih: n ≠ succ n
hs: succ n = succ (succ n)
succn = succ n
    apply succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_injn: MyNat
ih: n ≠ succ n
hs: succ n = succ (succ n)
succ.asucc n = succ (succ n)
    assumptionGoals accomplished! 🐙

Well that's a wrap on Advanced Addition World !

You can now move on to Advanced Multiplication World (after first doing Multiplication World, if you didn't do it already).