Goal:
    G : t  HI : invariants  x : Z  le : 0 <= x
  ============================
   ((if 0 <=? x then x else 0) = x)


DEBUG:Going to execute:
destruct (Z.leb_spec 0 x)
DEBUG LTAC Evaluated term: Z_of_to_label
DEBUG LTAC Evaluated term: Z_of_to_label

Goals:
    G : t  HI : invariants  x : Z  le : 0 <= x  H : 0 <= x
  ============================
   (x = x)

    G : t  HI : invariants  x : Z  le : 0 <= x  H : x < 0
  ============================
   (0 = x)


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: (Z.leb_spec 0 x)

Goals:
    G : t  HI : invariants  x : Z  le : 0 <= x  H : 0 <= x
  ============================
   (x = x)

    G : t  HI : invariants  x : Z  le : 0 <= x  H : x < 0
  ============================
   (0 = x)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3