theorem :: SERIES_5:35

for a, b being positive Real st a + b = 1 holds
((1 / (a ^2)) - 1) * ((1 / (b ^2)) - 1) >= 9