maybe T (\x => bitsToNat x e = Just n) $ natToBits n e k