Goal:
    G : t  HI : invariants  x : Nbar.t  y : Nbar.t
  ============================
   ((Some 0 <= x)%nbar ->
    to_label (max x y) = Nat.max (to_label x) (to_label y))


DEBUG:Going to execute:
destruct x

Goals:
    G : t  HI : invariants  z : Z  y : Nbar.t
  ============================
   ((Some 0 <= Some z)%nbar ->
    to_label (max (Some z) y) = Nat.max (to_label (Some z)) (to_label y))

    G : t  HI : invariants  y : Nbar.t
  ============================
   ((Some 0 <= None)%nbar ->
    to_label (max None y) = Nat.max (to_label None) (to_label y))


DEBUG:Going to execute:
intros H
DEBUG LTAC Evaluated term: x

Goals:
    G : t  HI : invariants  z : Z  y : Nbar.t  H : (Some 0 <= Some z)%nbar
  ============================
   (to_label (max (Some z) y) = Nat.max (to_label (Some z)) (to_label y))

    G : t  HI : invariants  y : Nbar.t  H : (Some 0 <= None)%nbar
  ============================
   (to_label (max None y) = Nat.max (to_label None) (to_label y))


DEBUG:Going to execute:
simpl in H

Goals:
    G : t  HI : invariants  z : Z  y : Nbar.t  H : 0 <= z
  ============================
   (to_label (max (Some z) y) = Nat.max (to_label (Some z)) (to_label y))

    G : t  HI : invariants  y : Nbar.t  H : False
  ============================
   (to_label (max None y) = Nat.max (to_label None) (to_label y))


DEBUG:Going to execute:
auto

Goals:
    G : t  HI : invariants  z : Z  y : Nbar.t  H : 0 <= z
  ============================
   (to_label (max (Some z) y) = Nat.max (to_label (Some z)) (to_label y))

    G : t  HI : invariants  y : Nbar.t  H : False
  ============================
   (to_label (max None y) = Nat.max (to_label None) (to_label y))


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