Goal:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z
  ============================
   (Z.max z z0 = Z.max z (if 0 <=? z0 then z0 else 0))


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

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
lia
DEBUG LTAC Evaluated term: (Z.leb_spec 0 z0)

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
Zify.zify; xlia zchecker

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
Zify.zify

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook; zify_saturate

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations;
            Zify.zify_post_hook

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs; Zify.zify_to_euclidean_division_equations

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op;
            Zify.zify_iter_specs

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let; zify_op

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook; zify_elim_let

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
intros

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
idtac

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
zify_elim_let

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@3>

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
zify_op

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
<coq-core.plugins.zify::TRANS@0>

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
Zify.zify_iter_specs

Goals:
    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : 0 <= z0
  ============================
   (Z.max z z0 = Z.max z z0)

    G : t  HI : invariants  z : Z  z0 : Z  H : 0 <= z  H0 : z0 < 0
  ============================
   (Z.max z z0 = Z.max z 0)


DEBUG:Going to execute:
fun => <coq-core.plugins.zify::ITER@0>

Goals:
  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : 0 <= z0
  z1 : Z
  H1 : z < z0 /\ z1 = z0 \/ z0 <= z /\ z1 = z
  ============================
   (z1 = z1)

  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : z0 < 0
  z1 : Z
  H1 : z < 0 /\ z1 = 0 \/ 0 <= z /\ z1 = z
  z2 : Z
  H2 : z < z0 /\ z2 = z0 \/ z0 <= z /\ z2 = z
  ============================
   (z2 = z1)


DEBUG:Going to execute:
Zify.zify_to_euclidean_division_equations

Goals:
  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : 0 <= z0
  z1 : Z
  H1 : z < z0 /\ z1 = z0 \/ z0 <= z /\ z1 = z
  ============================
   (z1 = z1)

  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : z0 < 0
  z1 : Z
  H1 : z < 0 /\ z1 = 0 \/ 0 <= z /\ z1 = z
  z2 : Z
  H2 : z < z0 /\ z2 = z0 \/ z0 <= z /\ z2 = z
  ============================
   (z2 = z1)


DEBUG:Going to execute:
lazymatch Zify.zify_convert_to_euclidean_division_equations_flag
           with
           | true =>
               Zify.zify_internal_to_euclidean_division_equations
           | false => idtac
           end

Goals:
  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : 0 <= z0
  z1 : Z
  H1 : z < z0 /\ z1 = z0 \/ z0 <= z /\ z1 = z
  ============================
   (z1 = z1)

  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : z0 < 0
  z1 : Z
  H1 : z < 0 /\ z1 = 0 \/ 0 <= z /\ z1 = z
  z2 : Z
  H2 : z < z0 /\ z2 = z0 \/ z0 <= z /\ z2 = z
  ============================
   (z2 = z1)


DEBUG:Going to execute:
Zify.zify_convert_to_euclidean_division_equations_flag

Goals:
  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : 0 <= z0
  z1 : Z
  H1 : z < z0 /\ z1 = z0 \/ z0 <= z /\ z1 = z
  ============================
   (z1 = z1)

  
  G : t
  HI : invariants
  z : Z
  z0 : Z
  H : 0 <= z
  H0 : z0 < 0
  z1 : Z
  H1 : z < 0 /\ z1 = 0 \/ 0 <= z /\ z1 = z
  z2 : Z
  H2 : z < z0 /\ z2 = z0 \/ z0 <= z /\ z2 = z
  ============================
   (z2 = z1)


DEBUG:Going to execute:
constr:(false)