Really Good Compression

When exam season arrives, many people start doing things they normally never do. This exam season, Sanggeun came up with a fantastic compression algorithm.

Using Sanggeun's algorithm, when you compress $N$ files, each file becomes at most $b$ bits after compression. It is hard to believe such a compression algorithm could exist, so write a program that decides whether such an algorithm is theoretically possible.

There are $N$ files to compress, all distinct, and each file consists of $1000$ bits. In other words, no two files are exactly the same.

The first line contains $N$ and $b$, separated by a space. ($1 \le N \le 10^{15}$, $0 \le b \le 50$)

Print yes if all $N$ files can be compressed so that each file is at most $b$ bits long, and no otherwise.