diff --git a/Game/Levels/Power/L01zero_pow_zero.lean b/Game/Levels/Power/L01zero_pow_zero.lean index c8f6818..6f51e6d 100644 --- a/Game/Levels/Power/L01zero_pow_zero.lean +++ b/Game/Levels/Power/L01zero_pow_zero.lean @@ -1,4 +1,5 @@ import Game.Levels.Multiplication +import Game.Levels.Algorithm import Game.MyNat.Power