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

Advanced Addition World

Level 5: add_right_cancel

The theorem add_right_cancel is the theorem that you can cancel on the right when you're doing addition -- if a + t = b + t then a = b. After intro h I'd recommend induction on t. Don't forget that rw [add_zero] at h can be used to do rewriting of hypotheses rather than the goal.

Theorem

On the set of natural numbers, addition has the right cancellation property. In other words, if there are natural numbers a, b and c such that a + t = b + t then we have a = b.

theorem 
add_right_cancel: ∀ (a t b : MyNat), a + t = b + t → a = b
add_right_cancel (
a: MyNat
a 
t: MyNat
t 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a + 
t: MyNat
t = 
b: MyNat
b + 
t: MyNat
t → 
a: MyNat
a = 
b: MyNat
b := by
a, t, b: MyNat
a + t = b + t → a = b
  intro 
h: a + t = b + t
h
a, t, b: MyNat
h: a + t = b + t
a = b
  induction 
t: MyNat
t with
a, t, b: MyNat
h: a + t = b + t
a = b
  | 
zero: MyNat
zero =>
a, b: MyNat
h: a + zero = b + zero
zero
a = b
    rw [
a, b: MyNat
h: a + zero = b + zero
zero
a = b
zero_is_0: zero = 0
zero_is_0
a, b: MyNat
h: a + 0 = b + 0
zero
a = b]
a, b: MyNat
h: a + 0 = b + 0
zero
a = b at 
h: a + zero = b + zero
h
a, b: MyNat
h: a + 0 = b + 0
zero
a = b
    rw [
a, b: MyNat
h: a + 0 = b + 0
zero
a = b
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
h: a = b + 0
zero
a = b]
a, b: MyNat
h: a = b + 0
zero
a = b at 
h: a + 0 = b + 0
h
a, b: MyNat
h: a = b + 0
zero
a = b
    rw [
a, b: MyNat
h: a = b + 0
zero
a = b
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
h: a = b
zero
a = b]
a, b: MyNat
h: a = b
zero
a = b at 
h: a = b + 0
h
a, b: MyNat
h: a = b
zero
a = b
    exact 
h: a = b
h
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
d: MyNat
d 
ih: a + d = b + d → a = b
ih =>
a, b, d: MyNat
ih: a + d = b + d → a = b
h: a + succ d = b + succ d
succ
a = b
    apply 
ih: a + d = b + d → a = b
ih
a, b, d: MyNat
ih: a + d = b + d → a = b
h: a + succ d = b + succ d
succ
a + d = b + d
    rw [
a, b, d: MyNat
ih: a + d = b + d → a = b
h: a + succ d = b + succ d
succ
a + d = b + d
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = b + succ d
succ
a + d = b + d]
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = b + succ d
succ
a + d = b + d at 
h: a + succ d = b + succ d
h
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = b + succ d
succ
a + d = b + d
    rw [
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = b + succ d
succ
a + d = b + d
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = succ (b + d)
succ
a + d = b + d]
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = succ (b + d)
succ
a + d = b + d at 
h: succ (a + d) = b + succ d
h
a, b, d: MyNat
ih: a + d = b + d → a = b
h: succ (a + d) = succ (b + d)
succ
a + d = b + d
    exact 
succ_inj: ∀ {a b : MyNat}, succ a = succ b → a = b
succ_inj 
h: succ (a + d) = succ (b + d)
h
Goals accomplished! 🐙

Next up Level 6