import MyNat.Addition
import MyNat.Multiplication
import AdditionWorld.Level1 -- zero_add
import AdditionWorld.Level5 -- one_eq_succ_zero
namespace MyNat
open MyNat

Multiplication World

Level 2: mul_one

In this level we'll need to use

• one_eq_succ_zero : 1 = succ 0

which was mentioned back in Addition World Level 5 and which will be a useful thing to rewrite right now, as we begin to prove a couple of lemmas about how 1 behaves with respect to multiplication.

Lemma

For any natural number m, we have m * 1 = m.

lemma 
mul_one: ∀ (m : MyNat), m * 1 = m
mul_one (
m: MyNat
m : 
MyNat: Type
MyNat) : 
m: MyNat
m * 
1: MyNat
1 = 
m: MyNat
m := by
m: MyNat
m * 1 = m
  rw [
m: MyNat
m * 1 = m
one_eq_succ_zero: 1 = succ 0
one_eq_succ_zero
m: MyNat
m * succ 0 = m]
m: MyNat
m * succ 0 = m
  rw [
m: MyNat
m * succ 0 = m
mul_succ: ∀ (a b : MyNat), a * succ b = a * b + a
mul_succ
m: MyNat
m * 0 + m = m]
m: MyNat
m * 0 + m = m
  rw [
m: MyNat
m * 0 + m = m
mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zero
m: MyNat
0 + m = m]
m: MyNat
0 + m = m
  rw [
m: MyNat
0 + m = m
zero_add: ∀ (n : MyNat), 0 + n = n
zero_add
m: MyNat
m = m]
Goals accomplished! 🐙

Notice how all our theorems are nicely building on each other.

Next up is Multiplication Level 3.