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


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrrewrite@0> $1 $2
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: Nat2Z.inj