proposition: Lemma mul_pow (a b n : mynat) : (a * b) ^ n = a ^ n * b ^ n.
proof: Proof. induction n. repeat rewrite pow_zero. rewrite mul_one. reflexivity. repeat rewrite pow_succ. rewrite IHn. rewrite mul_assoc. rewrite (mul_left_comm (b ^ n) _ _). 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