Mathé's 2-Angel proof is really nice, or at least the summary is appealing -- he imagines a 'nice' devil, shows it can be beaten, then proves that if you can beat the nice devil, you can beat the mean one.
This is one of my favorite problem solving strategies -- reducing to a more obvious solvable situation, then filling in the chinks and gaps to expand back.
The Kloster solution[0] solves it in a more direct way, by showing that for each action the devil takes the angel can take a counter action by limiting it's own moves.
In the one proof is the realization that sometimes it's easier to solve a smaller problem then prove equivalence to a harder problem, and in the other is the realization that sometimes voluntarily reducing the number of actions can lead to a simpler solution. Both are pretty good tools to have under one's belt.
Seems like Kloster devised a mathematical proof for a kiting - a game strategy that involves staying just out of the effective range of an opponent while they chase you.
This is one of my favorite problem solving strategies -- reducing to a more obvious solvable situation, then filling in the chinks and gaps to expand back.