Theorem Imo2024Q5.path2OfEdge0_firstMonster_eq_none_of_path1OfEdge0_firstMonster_eq_some

Modification history