proposition: Lemma pow_pow (a n m : mynat) : (a ^ n) ^ m = a ^ (n * m).
proof: Proof. induction m. rewrite mul_zero. repeat rewrite pow_zero. reflexivity. rewrite pow_succ. rewrite IHm. rewrite mul_succ. rewrite pow_add. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Pow Game.World.Addition Game.World.Multiplication