title: Is there a way to assert that the first digit (most significant) of number is a particular digit?
body: <p>I would like to assert that the most significant digit of a number is a particular value, but I don't actually know the length of the number. If it was the least significant digit, I know I could use the python mod (%) to check for it. But with an unknown number of digits, I'm unsure of how I could check this in z3.</p>
  <p>For example, I may know that the left most digit is a 9, such as 9x, or 9xx, or 9xxx etc.</p>
  <p>Thanks so much in advance</p>