Level 1 - The Lean Natural Numbers

import MyNat.Power
namespace MyNat
open MyNat

Level 1: `zero_pow_zero`

Given the lemma pow_zero which says m ^ 0 = 1 you can now prove zero to the power of zero is also one.

Lemma

0 ^ 0 = 1.

lemma zero_pow_zero: 0 ^ 0 = 1
zero_pow_zero : (0: MyNat
0 : MyNat: Type
MyNat) ^ (0: MyNat
0 : MyNat: Type
MyNat) = 1: MyNat
1 := by0 ^ 0 = 1
  rw [0 ^ 0 = 1pow_zero: ∀ (m : MyNat), m ^ 0 = 1
pow_zero1 = 1]Goals accomplished! 🐙

That was easy! Next up Level 2