proposition: Lemma mul_left_comm (a b c : mynat) : a * (b * c) = b * (a * c).
proof: Proof. rewrite mul_comm. rewrite mul_assoc. rewrite (mul_comm c a). reflexivity. Qed.
imports: Unicode.Utf8 Game.Mynat.Definition Game.Mynat.Add Game.Mynat.Mul Game.World.Addition