Goal:
  
  G : t
  invG : invariants G
  acG : acyclic_no_loop G
  l : labelling
  Hl : correct_labelling G l
  x : V.t
  k : nat
  d := Some (Z.of_nat (k + l x)) : option Z
  Hk : (lsp G x (s G) + d <= Some 0)%nbar
  Hledge : forall e : EdgeSet.elt,
           EdgeSet.In e (E G) ->
           Z.of_nat (l e..s) + e..w <= Z.of_nat (l e..t)
  s : V.t
  w : Z
  t : V.t
  he : EdgeSet.In (s, w, t) (E G)
  u : nat
  hs : VSet.In (s, w, t)..s (V G)
  ht : VSet.In (s, w, t)..t (V G)
  _n_ : nat
  Hledge0 : Z.of_nat (l s) + w <= Z.of_nat (l t)
  _a_ : Z
  _a1_ : Z
  h : _a_ + w <= _a1_
  heq_u : Z.of_nat u = Z.of_nat (to_label (lsp G x (s, w, t)..s + d)%nbar)
  z8 : Z
  E0 : z8 = Z.of_nat _n_ + 1
  ule : Z.of_nat (l s) <= Z.of_nat _n_ + 1
  Hl0 : Z.of_nat (l (WeightedGraph.s G)) = 0
  cstr : 0 <= Z.of_nat (l (WeightedGraph.s G))
  cstr0 : 0 <= Z.of_nat k
  cstr1 : 0 <= Z.of_nat (to_label (lsp G x (s, w, t)..s + d)%nbar)
  cstr2 : 0 <= Z.of_nat (l x)
  cstr3 : 0 <= Z.of_nat _n_
  cstr4 : 0 <= Z.of_nat (l t)
  cstr5 : 0 <= Z.of_nat (l s)
  cstr6 : 0 <= Z.of_nat u
  z7 : Z
  H7 : 0 < _a1_ + (Z.of_nat k + Z.of_nat (l x)) /\
       z7 = _a1_ + (Z.of_nat k + Z.of_nat (l x)) \/
       _a1_ + (Z.of_nat k + Z.of_nat (l x)) <= 0 /\ z7 = 0
  H8 : 0 < _a_ + (Z.of_nat k + Z.of_nat (l x)) /\
       z8 = _a_ + (Z.of_nat k + Z.of_nat (l x)) \/
       _a_ + (Z.of_nat k + Z.of_nat (l x)) <= 0 /\ z8 = 0
  ============================
   (z8 + w <= z7)


DEBUG:Going to execute:
zify_saturate