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