import MyNat.Definition
import MyNat.Addition
import AdditionWorld.Level6
namespace MyNat
open MyNat

axiom 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj {
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat} : 
succ: MyNat → MyNat
succ 
a: MyNat
a = 
succ: MyNat → MyNat
succ 
b: MyNat
b → 
a: MyNat
a = 
b: MyNat
b

Advanced Addition World

Level 1: succ_inj. A function.

Let's learn how to use succ_inj. You should know a couple of ways to prove the below -- one directly using an exact, and one which uses an apply first. But either way you'll need to use succ_inj.

Theorem

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

theorem 
succ_inj': ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj' {
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat} (
hs: succ a = succ b
hs : 
succ: MyNat → MyNat
succ 
a: MyNat
a = 
succ: MyNat → MyNat
succ 
b: MyNat
b) :  
a: MyNat
a = 
b: MyNat
b := by
a, b: MyNat
hs: succ a = succ b
a = b
  exact 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj 
hs: succ a = succ b
hs
Goals accomplished! 🐙

Important thing.

You can rewrite proofs of equalities. If h : A = B then rw [h] changes As to Bs. But you cannot rewrite proofs of implications. rw [succ_inj] will never work because succ_inj isn't of the form A = B, it's of the form A⟹ B. This is one of the most common mistakes I see from beginners. ⟹ and = are two different things and you need to be clear about which one you are using.

Next up Level 2