for i, n being Nat
for a, b being non negative Real holds ((a,b) In_Power n) . i >= ((a,b) Subnomial n) . i