theorem Th25: :: LIOUVIL1:26

for b, i being Nat st b >= 1 holds
(powerfact b) . i <= ((1 / b) GeoSeq) . i