import MyNat.Definition
import MyNat.Addition
import AdditionWorld.Level4 -- add_comm
import AdvancedAdditionWorld.Level10 -- add_left_eq_zero
namespace MyNat
open MyNat

Advanced Addition World

Level 11: add_right_eq_zero

We just proved add_left_eq_zero (a b : MyNat) : a + b = 0 → b = 0. Hopefully add_right_eq_zero shouldn't be too hard now.

Lemma

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

lemma 
add_right_eq_zero: ∀ {a b : MyNat}, a + b = 0 → a = 0
add_right_eq_zero {
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat} : 
a: MyNat
a + 
b: MyNat
b = 
0: MyNat
0 → 
a: MyNat
a = 
0: MyNat
0 := by
a, b: MyNat
a + b = 0 → a = 0
  intro 
h: a + b = 0
h
a, b: MyNat
h: a + b = 0
a = 0
  rw [
a, b: MyNat
h: a + b = 0
a = 0
add_comm: ∀ (a b : MyNat), a + b = b + a
add_comm
a, b: MyNat
h: b + a = 0
a = 0]
a, b: MyNat
h: b + a = 0
a = 0 at 
h: a + b = 0
h
a, b: MyNat
h: b + a = 0
a = 0
  exact 
add_left_eq_zero: ∀ ⦃a b : MyNat⦄, a + b = 0 → b = 0
add_left_eq_zero 
h: b + a = 0
h
Goals accomplished! 🐙

Next up Level 12