proposition: Lemma one_pow (n : mynat) : (1 : mynat) ^ n = 1.
proof: Proof. induction n. reflexivity. rewrite pow_succ. rewrite IHn. rewrite mul_one. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Pow Game.World.Addition Game.World.Multiplication