for x being Nat holds x < 2 to_power (LenBSeq x)