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