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