Goal:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (diff l _x2_..s _x2_..t + (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
unfold diff

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
lia

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
Zify.zify

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
intros; Zify.zify_pre_hook

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
intros

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
Zify.zify_pre_hook

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
idtac

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
zify_elim_let

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
zify_op

Goals:
    G : t  l : labelling  Gl := relabel G l : t  x : V.t  y : V.t  _x_ : V.t
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
Zify.zify_iter_specs

Goals:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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

Goals:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
Zify.zify_to_euclidean_division_equations

Goals:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


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
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
Zify.zify_convert_to_euclidean_division_equations_flag

Goals:
  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _x_ : V.t
  cstr : 0 <= Z.of_nat (l _x_)
  ============================
   (0 = Z.of_nat (l _x_) - Z.of_nat (l _x_))

  
  G : t
  l : labelling
  Gl := relabel G l : t
  x : V.t
  y : V.t
  _z_ : V.t
  _x2_ : Edge.t
  _b_ : EdgeSet.In _x2_ (E G)
  _p_ : PathOf Gl _x2_..t _z_
  cstr : 0 <= Z.of_nat (l _x2_..s)
  cstr0 : 0 <= Z.of_nat (l _z_)
  cstr1 : 0 <= Z.of_nat (l _x2_..t)
  ============================
   (Z.of_nat (l _x2_..t) - Z.of_nat (l _x2_..s) +
    (Z.of_nat (l _z_) - Z.of_nat (l _x2_..t)) =
    Z.of_nat (l _z_) - Z.of_nat (l _x2_..s))


DEBUG:Going to execute:
constr:(false)