Ah yes, PMW was mentioned to me but I never quite got round to looking at it. It looks to be on roughly the same general level of complexity as Mus (my own unpublished effort as mentioned above). A brief look at its font in particular doesn't do anything to make me think I've been wasting my time, though :-)

The theorem: given a positive integer n, how many integers do you need in order to guarantee that n of them sum to a multiple of n? (answer and five different proofs) I think it took us about an afternoon or so of serious thought between us to find a proof, once we'd decided what we thought the right answer was to start with (for which I cheated by computer search). Of the five proofs given there, ours was pretty similar to the first one (though Erdős's version, as one might expect, was more elegant and included a more neatly reusable lemma).