Goal:
  
  b : Byte.byte
  x : string
  IHx : forall y : string,
        CompareSpec (x = y) (lt x y) (lt y x) (compare x y)
  b0 : Byte.byte
  y : string
  H : ByteCompare.compare b0 b = Lt
  ============================
   (CompareSpec (String b x = String b0 y) (Gt = Lt)
      (match ByteCompare.compare b0 b with
       | Eq => compare y x
       | Lt => Lt
       | Gt => Gt
       end = Lt) Gt)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2