Simplifying Z3 Expressions

I am using z3 in Python to simplify some boolean expressions and I have a question. When I execute the following code

x = BitVec('x', 8)
e = ULT(x - 5, 10)
Then('simplify', 'propagate-values', 'ctx-solver-simplify')(e).as_expr()

      

        
        
        
      

    

I get the result:

Not(ULE(10, 251 + x))

      

        
        
        
      

    

However, this is equivalent to

And(UGE(x, 5), ULT(x, 15))

      

        
        
        
      

    

Is there a way to convert (simplify) the first expression (Not) to the second (And)? More specifically, can you ask z3 about the ranges of values ​​that a particular variable can take (in this example, x> = 5 & x <15)?