theorem :: SERIES_5:36

for a, b being positive Real st a + b = 1 holds
(a * b) + (1 / (a * b)) >= 17 / 4