proposition: Lemma zero_pow_succ (a : mynat) : (0 : mynat) ^ (succ a) = 0.
proof: Proof. rewrite pow_succ. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Pow Game.World.Addition Game.World.Multiplication