RE: https://mathstodon.xyz/@skelk/116174927025037600 Now with an AI-assisted and LEAN formalized proof, available at https://woutercvb.github.io/greedy_by_finish_time_draft22april2026.pdf