theorem SLT: :: NEWTON04:84

for a, b being non negative Real
for n being non zero Nat holds (a |^ n) + (b |^ n) <= Sum ((a,b) Subnomial n)