import MyNat.Definition
import MyNat.Addition -- add_zero
import AdvancedAdditionWorld.Level6 -- add_left_cancel
namespace MyNat
open MyNat

Advanced Addition World

Level 8: eq_zero_of_add_right_eq_self

The lemma you're about to prove will be useful when we want to prove that ≤ is antisymmetric. There are some wrong paths that you can take with this one.

Lemma

If a and b are natural numbers such that a + b = a, then b = 0.

lemma 
eq_zero_of_add_right_eq_self: ∀ {a b : MyNat}, a + b = a → b = 0
eq_zero_of_add_right_eq_self {
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat} : 
a: MyNat
a + 
b: MyNat
b = 
a: MyNat
a → 
b: MyNat
b = 
0: MyNat
0 := by
a, b: MyNat
a + b = a → b = 0
  intro 
h: a + b = a
h
a, b: MyNat
h: a + b = a
b = 0
  apply 
add_left_cancel: ∀ (t a b : MyNat), t + a = t + b → a = b
add_left_cancel 
a: MyNat
a
a, b: MyNat
h: a + b = a
a
a + b = a + 0
  rw [
a, b: MyNat
h: a + b = a
a
a + b = a + 0
h: a + b = a
h
a, b: MyNat
h: a + b = a
a
a = a + 0]
a, b: MyNat
h: a + b = a
a
a = a + 0
  rw [
a, b: MyNat
h: a + b = a
a
a = a + 0
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a, b: MyNat
h: a + b = a
a
a = a]
Goals accomplished! 🐙

Remember from FunctionWorld Level 4../FunctonWorld/Level4.lean.md) that the apply tactic is can construct the path backwards? Well when we use it with add_left_cancel a it results in the opposite of cancellation, it results in adding a to both sides changing the goal from ⊢ b = 0 to ⊢ a + b = a + 0. This then allows us to use our hypothesis h : a + b = a in rw to complete the proof.

Next up Level 9