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

Advanced Addition World

Level 2: `succ_succ_inj`

In the below theorem, we need to apply succ_inj twice. Once to prove succ (succ a) = succ (succ b) ⟹ succ a = succ b, and then again to prove succ a = succ b ⟹ a = b. However succ a = succ b is nowhere to be found, it's neither an assumption or a goal when we start this level. You can make it with have or you can use apply.

Theorem : succ_succ_inj

For all naturals a and b, if we assume succ (succ a) = succ (succ b), then we can deduce a = b.

theorem succ_succ_inj: ∀ {a b : MyNat}, succ (succ a) = succ (succ b) → a = b
succ_succ_inj {a: MyNat
a b: MyNat
b : MyNat: Type
MyNat} (h: succ (succ a) = succ (succ b)
h : succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ a: MyNat
a) = succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ b: MyNat
b)) :  a: MyNat
a = b: MyNat
b := bya, b: MyNat
h: succ (succ a) = succ (succ b)
a = b
  apply succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inja, b: MyNat
h: succ (succ a) = succ (succ b)
asucc a = succ b
  apply succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inja, b: MyNat
h: succ (succ a) = succ (succ b)
a.asucc (succ a) = succ (succ b)
  exact h: succ (succ a) = succ (succ b)
hGoals accomplished! 🐙

Other solutions

Make sure you understand them all. And remember that rw should not be used with succ_inj -- rw works only with equalities or ↔ statements, not implications or functions.

example: ∀ {a b : MyNat}, succ (succ a) = succ (succ b) → a = b
example {a: MyNat
a b: MyNat
b : MyNat: Type
MyNat} (h: succ (succ a) = succ (succ b)
h : succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ a: MyNat
a) = succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ b: MyNat
b)) :  a: MyNat
a = b: MyNat
b := bya, b: MyNat
h: succ (succ a) = succ (succ b)
a = b
  apply succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inja, b: MyNat
h: succ (succ a) = succ (succ b)
asucc a = succ b
  exact succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj h: succ (succ a) = succ (succ b)
hGoals accomplished! 🐙

example: ∀ {a b : MyNat}, succ (succ a) = succ (succ b) → a = b
example {a: MyNat
a b: MyNat
b : MyNat: Type
MyNat} (h: succ (succ a) = succ (succ b)
h : succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ a: MyNat
a) = succ: MyNat → MyNat
succ (succ: MyNat → MyNat
succ b: MyNat
b)) :  a: MyNat
a = b: MyNat
b := bya, b: MyNat
h: succ (succ a) = succ (succ b)
a = b
  exact succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj (succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj h: succ (succ a) = succ (succ b)
h)Goals accomplished! 🐙

Next up Level 3