This is one of my favorite original, short proofs. The proof gives a closed form minimum for a certain function that acts on arbitrary-length boolean vectors and returns an integer. Additionally, the vector has a fixed Hamming Weight.
Here's a description with symbols:
You can read the PDF in Github here or embedded in HTML here.
To build the proof html, simply run:
htlatex ProofSample.tex