proposition: Lemma pow_one (a : mynat) : a ^ (1 : mynat) = a.
proof: Proof. rewrite one_eq_succ_zero. rewrite pow_succ. rewrite pow_zero. rewrite one_mul. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.Mynat.Pow Game.World.Addition Game.World.Multiplication