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_
  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:
idtac

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_post_hook

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:
idtac

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_saturate

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:
<coq-core.plugins.zify::TRANS@1>

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:
xlia zchecker

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:
<coq-core.plugins.micromega::Lia@0> $1