import MyNat.Addition -- imports addition.
import AdditionWorld.Level1 -- zero_add
import AdditionWorld.Level3 -- succ_add
namespace MyNat
open MyNat

Addition World

Level 4: add_comm

In this level, you'll prove that addition is commutative.

Lemma

On the set of natural numbers, addition is commutative. In other words, for all natural numbers a and b, we have a + b = b + a.

lemma 
add_comm: ∀ (a b : MyNat), a + b = b + a
add_comm (
a: MyNat
a 
b: MyNat
b : 
MyNat: Type
MyNat) : 
a: MyNat
a + 
b: MyNat
b = 
b: MyNat
b + 
a: MyNat
a := by
a, b: MyNat
a + b = b + a
  induction 
b: MyNat
b with
a, b: MyNat
a + b = b + a
  | 
zero: MyNat
zero =>
a: MyNat
zero
a + zero = zero + a
    rw [
a: MyNat
zero
a + zero = zero + a
zero_is_0: zero = 0
zero_is_0
a: MyNat
zero
a + 0 = 0 + a]
a: MyNat
zero
a + 0 = 0 + a
    rw [
a: MyNat
zero
a + 0 = 0 + a
add_zero: ∀ (a : MyNat), a + 0 = a
add_zero
a: MyNat
zero
a = 0 + a]
a: MyNat
zero
a = 0 + a
    rw [
a: MyNat
zero
a = 0 + a
zero_add: ∀ (n : MyNat), 0 + n = n
zero_add
a: MyNat
zero
a = a]
Goals accomplished! 🐙
  | 
succ: MyNat → MyNat
succ 
b: MyNat
b 
ih: a + b = b + a
ih =>
a, b: MyNat
ih: a + b = b + a
succ
a + succ b = succ b + a
    rw [
a, b: MyNat
ih: a + b = b + a
succ
a + succ b = succ b + a
add_succ: ∀ (a d : MyNat), a + succ d = succ (a + d)
add_succ
a, b: MyNat
ih: a + b = b + a
succ
succ (a + b) = succ b + a]
a, b: MyNat
ih: a + b = b + a
succ
succ (a + b) = succ b + a
    rw [
a, b: MyNat
ih: a + b = b + a
succ
succ (a + b) = succ b + a
ih: a + b = b + a
ih
a, b: MyNat
ih: a + b = b + a
succ
succ (b + a) = succ b + a]
a, b: MyNat
ih: a + b = b + a
succ
succ (b + a) = succ b + a
    rw [
a, b: MyNat
ih: a + b = b + a
succ
succ (b + a) = succ b + a
succ_add: ∀ (a b : MyNat), succ a + b = succ (a + b)
succ_add
a, b: MyNat
ih: a + b = b + a
succ
succ (b + a) = succ (b + a)]
Goals accomplished! 🐙

If you are keeping up so far then nice! You're nearly ready to make a choice: Multiplication World or Function World. But there are just a couple more useful lemmas in Addition World which you should prove first.

Press on to level 5.