theorem SAB: :: NEWTON04:64
for a, b being Real
for n being Nat holds (a,b) Subnomial n = Rev ((b,a) Subnomial n)