import MyNat.Power
import AdditionWorld.Level5 -- one_eq_succ_zero
import MultiplicationWorld.Level3 -- one_mul
namespace MyNat
open MyNat

Power World

Level 3: pow_one

Lemma

For all naturals a, a ^ 1 = a.

lemma 
pow_one: ∀ (a : MyNat), a ^ 1 = a
pow_one (
a: MyNat
a : 
MyNat: Type
MyNat) : 
a: MyNat
a ^ (
1: MyNat
1 : 
MyNat: Type
MyNat) = 
a: MyNat
a := by
a: MyNat
a ^ 1 = a
  rw [
a: MyNat
a ^ 1 = a
one_eq_succ_zero: 1 = succ 0
one_eq_succ_zero
a: MyNat
a ^ succ 0 = a]
a: MyNat
a ^ succ 0 = a
  rw [
a: MyNat
a ^ succ 0 = a
pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succ
a: MyNat
a ^ 0 * a = a]
a: MyNat
a ^ 0 * a = a
  rw [
a: MyNat
a ^ 0 * a = a
pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero
a: MyNat
1 * a = a]
a: MyNat
1 * a = a
  rw [
a: MyNat
1 * a = a
one_mul: ∀ (m : MyNat), 1 * m = m
one_mul
a: MyNat
a = a]
Goals accomplished! 🐙

Next up Level 4