Theorem Imo2024Q5.Path.mem_of_firstMonster_eq_some

Modification history