Abstract
This is a formalisation of the proof of an inequality by Trevor D. Wooley attesting that when
,
with equality if and only if for some positive integer .
The source is the note An Elementary Discrete Inequality by T. D. Wooley.
Angeliki Koutsoukou-Argyraki 🌐 📧
October 2, 2024