[Sebb767]

I think he's missing two important points.

Firstly, when you break down your proof on the pigeonhole principle, you've shown that the problem reduces to something simple and understandable. It's basically a nicer version of "q.e.d.".

Secondly, and much more important: Integrating the principle allows the reader to understand the end of the proof more easily. I.e., if I find the principle mentioned in the end, I know that I need to look for "pigeons" and "holes" and that the proof is a way to get to those - allowing me to understand the proof from the conclusion going backwards, or at least helps doing so.

Of course, this varies per person and depends a bit on how much you're trained in reading proofs, too. But it's enough to justify naming it in my opinion.

[impendia]

Strongly agreed. I've taught university-level discrete math several times, and beginners to the subject need pegs to hang their hat on, something that serves as a goal and a signal that they're done. The Pigeonhole Principle is an ideal example of this.

Conversely, in research papers, or in conversations among math researchers (at least in my discipline) the Pigeonhole Principle is seldom mentioned by name. The idea is considered too "obvious" to need a name.