for n, b being Nat st b > 1 & n >= 1 holds
Sum ((b - 1) (#) ((powerfact b) ^\ (n + 1))) < 1 / ((b to_power (n !)) to_power n)