proposition: Lemma mul_comm (a b : mynat) : a * b = b * a.
proof: Proof. induction b. rewrite zero_mul. reflexivity. rewrite mul_succ. rewrite succ_mul. rewrite IHb. reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition