import PowerWorld.Level1
import MyNat.Multiplication -- mul_zero
namespace MyNat
open MyNat

Power World

Level 2: `zero_pow_succ`

Lemma

For all naturals m, 0 ^ (succ m) = 0.

lemma zero_pow_succ: ∀ (m : MyNat), 0 ^ succ m = 0
zero_pow_succ (m: MyNat
m : MyNat: Type
MyNat) : (0: MyNat
0 : MyNat: Type
MyNat) ^ (succ: MyNat → MyNat
succ m: MyNat
m) = 0: MyNat
0 := bym: MyNat
0 ^ succ m = 0
  rw [m: MyNat
0 ^ succ m = 0pow_succ: ∀ (m n : MyNat), m ^ succ n = m ^ n * m
pow_succm: MyNat
0 ^ m * 0 = 0]m: MyNat
0 ^ m * 0 = 0
  rw [m: MyNat
0 ^ m * 0 = 0mul_zero: ∀ (a : MyNat), a * 0 = 0
mul_zerom: MyNat
0 = 0]Goals accomplished! 🐙

Next up Level 3