  This paper formalize the existence's proof of first-integrals for any second
order ODE, allowing to discriminate periodic orbits. Up to the author's
knowledge, such a powerful result is not available in the literature providing
a tool to determine periodic orbits/limit cycles in the most general scenario.
