A typo, this bit has one quote mark too many:

> Since they're both the least, we must have a≤a′ and a′≤a′. This doesn't imply a=a′ , in general!