Goal:
    G : t  HI : invariants  z : Z
  ============================
   (Z.of_nat match z with
             | Z.pos p => Pos.to_nat p
             | _ => 0
             end = (if 0 <=? z then z else 0))


DEBUG:Going to execute:
destruct z

Goals:
    G : t  HI : invariants
  ============================
   (Z.of_nat 0 = (if 0 <=? 0 then 0 else 0))

    G : t  HI : invariants  p : positive
  ============================
   (Z.of_nat (Pos.to_nat p) = (if 0 <=? Z.pos p then Z.pos p else 0))

    G : t  HI : invariants  p : positive
  ============================
   (Z.of_nat 0 = (if 0 <=? Z.neg p then Z.neg p else 0))


DEBUG:Going to execute:
auto
DEBUG LTAC Evaluated term: z

Goals:
    G : t  HI : invariants
  ============================
   (Z.of_nat 0 = (if 0 <=? 0 then 0 else 0))

    G : t  HI : invariants  p : positive
  ============================
   (Z.of_nat (Pos.to_nat p) = (if 0 <=? Z.pos p then Z.pos p else 0))

    G : t  HI : invariants  p : positive
  ============================
   (Z.of_nat 0 = (if 0 <=? Z.neg p then Z.neg p else 0))


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