HOL-ex.Birthday_Paradox