Goal:
  
  b : Byte.byte
  x : string
  IHx : forall y z : t,
        compare x y = Lt -> compare y z = Lt -> compare x z = Lt
  y : string
  b1 : Byte.byte
  H : ByteCompare.compare b b1 = Lt
  z : string
  ============================
   (compare y z = Lt -> Lt = Lt)


DEBUG:Going to execute:
solve
[ trivial
with eq_true
| Ltac.reflexivity
| Ltac.symmetry; trivial
| contradiction ]